Dr. David Matuszek,
david.l.matuszek@lmco.com
Summer 1998, Villanova University
Write a program to do simple (variable-free) resolution on two clauses. By "variable free," I mean that two literals can be unified if and only if they are identical. For example, 'abc unifies with 'abc, and nothing else. This is so that you don't have to deal with the complexities of unification.
You will need some way of representing clauses and negated literals. An obvious way to represent a clause is as a list of literals; one way to represent the negation of 'abc is as '(not abc). Thus, the clause "poor v -smart v happy" might be represented as
'(poor (not smart) happy)
Your function should take two such clauses, resolve them, and return the result. If no resolution can be found, the boolean value #f should be returned instead. For example, the function call:
(resolve '(t (not o) a (not d)) '(t a d (not p) (not o) l (not e)))
should give the result:
'(t (not o) a (not p) l (not e))
where the order of the literals in the result is not important.
Reminder: to do resolution, find a literal that is negated in one clause but not the other; then combine the two clauses, omitting this literal, and return a clause that has exactly one copy of each other literal.
If a pair of clauses has two different literals that may be used for resolution, then you need to resolve on only one of the literals. In variable-free resolution, the result will always be a clause that simplifies to TRUE (not necessarily the case in more complex resolutions!); for example, resolving
'(poor (not smart) happy) with '((not poor) smart happy)
gives
'(smart (not smart) happy)
and, since "smart or not smart" is always TRUE, the result must be TRUE. For a little extra credit you can check for this case and return #t, but I won't require it.
Turn in: