| Date: 4/21 | Title: Program 3 - using mapcar to extract predicates for duplicate check |
> I have it correctly changing the variable names, but now duplicate checking
> seems impossible. Is there a way to check duplicates when all the variables
> have different names? I don't know LISP well enough to check the size of
> the atom, or whether it starts with a 'G'.
First, run it without the duplicate check.
You can use the "mapcar" function to extract just the predicate symbols.
> (setq clause '(((P X) (Q (F X))) ((R X Y))))
(((P X) (Q (F X))) ((R X Y)))
>(mapcar #'car (first clause))
(P Q)
>(mapcar #'car (second clause))
(R)
and the compare the resulting list.
|
| Date: 4/21 | Title: Program 3 - using unique symbols for variables for unification |
> After you get a resolvent, how do you replace the old variables with new
> ones using (intern...)? How can you decide which values in the list
> need changed?
If the literal pair did not have to be unified, you can just combine
the two clauses by
1. taking out the complementary literals, and
2. combine the two clauses by joining the
two positive literal lists, and then the two negative literal
lists.
If you had to unify the two literals, then the resulting substitution
is what you need to apply to both clauses, using (sublis ...).
> Yes I did that part, but now some of the new clauses have the same variables
> as the clauses before it. Unify wont work when the same variable appears in
> both sides, so the intructions say to change the variables using (intern
> (symbol-name (gynsym))) How can you decide which parts of the resolvent
> clause to change, and which to leave the same? That is, if you use (atom..)
> to change variables, it would change function names too.
I see what you mean.
In that case, by default, replace the variables with unique ones.
Generate a alist by doing
(setq subs (cons 'x (intern (symbol-name (gensym)))))
and apply that to the list with sublis
> (sublis (list subs) '( ((p x) (q (f x))) ( (r x y) ) ))
(((P G1065) (Q (F G1065))) ((R G1065 Y)))
To find out the variables, you have to inspect each literal, one by one.
For each literal, you should look at the 2nd 3rd ... arguments and
find all those that are atoms.
|
| Date: 4/21 | Title: Program 3 - how to extract elements from an alist |
> When unify is run against two expressions such as (howl v) and (howl x) it
> produces a list like (v . x)
>
> How do I access x in this list?
>
Simply do cdr.
>(setq s (cons 'a 'b))
(A . B)
>(cdr s)
B
|
| Date: 4/21 | Title: Program 3 - resolving and adding new clauses |
> First, in the discussion of the algorithm in the
> assignment, it makes it seem like the only way that we
> add to the resolvent is if we can find a common
> variable between the pos and neg lists of two clauses.
> Should we also add the two clauses combined as a whole
> to the resolvent? For example:
You must
1. unify the complementary literals
2. remove the unified literals from both
clauses, and combine the remainder in
a new clause, and add that to the end of the
clause list.
- in the following case, P(x) and ~P(z), for one
resulting resolved clause, and P(a) and ~P(z),
for another clause.
>
> If we had clauses
>
> (1 ((P x) (P a) (Q x y)) nil)
> (2 ((R z)) ((P z)))
>
> Should we also add the combined clause to the list:
> (# ((P x) (P a) (Q x y) (R z)) ((P z)))
No. It should result in two clauses
(# ((P a) (Q x y) (R x)) NIL)
or
(# ((P x) (Q x y) (R a)) NIL)
> It would seem like if we do this the list would get
> infinetly larger and larger. However, it seems like if
Now you know it won't.
> we dont add anytime but when they have a common
> variable then it will return an empty resolvent before
> it has actually reached resolution.
Only after you have exhausted all possible clause pairs.
> If we had clauses to resolve:
> (1 ((P x)) ((Q y)))
> (2 ((Howls z)) nil)
> then because there are no common clauses between the
> positive and negative lists, it would return an empty
> resolvent.
Yes, in this case, you don't have enough facts to
prove anything.
> Mainly I don't understand the stipulation that the
> main loop of the algorithm is done, assumed false when
> resolve returns an empty resolvent.
Your example above is a perfect example why
the algorithm should terminate in such a case.
|
| Date: 4/09 | Title: Program 3 clarifications |
Here are some clarifications on program #3.
- You may ignore the unit-preference requirement (this is
section 3.4).
- When you have clauses like the following
P(x) \/ P(a) \/ Q(x,y) (1)
~P(z) \/ R(z) (2)
generate all possible combinations that are resolvable. For example,
in this case, it would be:
{x/z} : P(a) \/ Q(z,y) \/ R(z)
{z/a} : P(x) \/ Q(x,y) \/ R(a)
- When checking for duplicate clauses, you don't have
to be very thorough. Just check the most limited case,
for example, using (equal ...).
|
| Date: 2/04 | Title: Divide by zero |
Question:
> I have a question about program #1:
>
> I have already implemented several simplification routines. For my divide
> by 0 checks I catch explicit divide by 0 errors such as:
> (/ x 0) and (/ x (- 3 3))
> and I catch this kind as well:
> (/ x (- x x)) and (/ 3 (- (+ x 1) (+ x 1)))
> but I wouldn't catch:
> (/ x (+ x (- x))) or (/ 3 (- (+ 1 x) (+ x 1)))
>
> Is it okay to miss those simplifications?
>
Answer:
Sure. To detect things like that you have to go deeper than
what the simplistic scheme we are using now would allow, and
it is out of the scope of the current exercise.
|