The pattern matcher you will write has been described in class—the Unify function. In fact, since I’m feeling magnanimous, I’ll even you a Unify implementation in Lisp. You can find it on the website on the Assignments page.

You should consider the code provided as a starting point or guide rather than as something you can just use “out of the box”—you’ll almost certainly need to change it for your purposes. For example, you may have to change it and its supporting functions to conform to your representation of predicate calculus. (Some suggestions for how to represent predicate calculus are in the comments in Lisp code.) You may also have to modify the Unify function to handle ORs and NOTs, if you represent them explicitly or have multiple negation in an axiom.suggest).

Note that there are some functions a “read macro” in the code to help with handling variables, which by convention are symbols starting with the character “?”, e.g., ?x. For example,

        (variable? '?foo)

returns t,

        (varname '?foo)

will return FOO, and

        (make-var 'bar)

will return ?BAR. There are also functions to help generate new symbols based on old symbols. For example,

        (newSymbol '?foo))

or

        (newSymbol '?foo3)

will both return a unique variable whose name is based on FOO; if ?foo3 is the last variable created in the “foo” series, then either of these calls will return ?FOO4.

The file also contains a function, instantiate, that will replace all variables in an expression (e.g., a literal or clause) with their bindings. See the file for more information.

The knowledge bases for your program are sets of clauses. Each clause is a list-structured version of a predicate calculus clause. For example, the predicate calculus clause: \[\neg{}Roman(x_2) \vee loyalto(x_2,Caesar) \vee hate(x_2,Caesar)\] which could come from the axiom: \[\forall\ x_2\ Roman(x_2) \wedge \neg{}loyalto(x_2,Caesar) \Longrightarrow hates(x_2,Caesar)\] could be represented in your program as:

            (or (not (Roman ?x2))
                (loyalto ?x2 Caesar)
                (hate ?x2 Caesar))

This representation implies several things. First of all, you will need to make your program smart enough to recognize OR (unless you figure out a trick to get rid of OR) and NOT—that is, it needs to know such things as “(not (Roman Marcus)) is the negation of (Roman Marcus)”. It also needs to know how to access each term of an OR’ed clause.

Finally, it has to have a way of knowing what things are variables. I suggest using the question mark prefix discussed above. An alternative is to use property lists of symbols to determine if they are variables. For example,

(defun make-var (symbol)
  (setf (getf symbol 'var) t)
  symbol)

(defun is-var (symbol)
  (getf symbol 'var))

defines two functions, one to set the var property of a symbol to t and another to return t if the property is set.

This is the portion of the program that actually does resolution, as well as decides on which clauses to use. General algorithms for this were given in class and in your text.

Note that your program must have the ability to know when it reaches a dead end. If there was more than one way to do resolution at some point (multiple clauses that could be resolved, multiple literals within a clause that could resolve with another clause, etc.), then if one doesn’t work, it should try another until no more are possible; then it should backtrack. If this reminds you of depth-first search, it should.¹ Your program must also be able to backtrack to try different variable bindings, when more than one is found. You should think carefully about which control strategy(ies) you want to use to select clauses (e.g., set of support, etc.) and stick to it (them).

Your program must handle variables—you should show their use in the script you turn in.

Don’t forget to deal with the fact that resolution theorem proving is semi-decidable!

Your program’s output should be sufficiently detailed to show off your program. If some capability it has isn’t shown, we will assume that it can’t do it. It should also be clear to the reader what is being output by the program. This means that you should have the program nicely format its output and clearly label things that you want the reader to understand. If we can’t understand your output, you won’t get credit for it.

You should turn in several examples of your program proving things, and one example of it not being able to prove something.

You should also print out the knowledge base used prior to each set of sample runs of the program.

You will turn in your program, script file, and write-up using Blackboard, as usual. You do not need to turn in a copy of unify.lisp! Turn in a zipfile or a gzip’d tarfile. Your write-up must be in PDF form!

Your program must be well-documented, especially with respect to the axioms you provide the program with. For each clause, describe what it means—both in predicate calculus and in English.

It is important that you provide good instructions in your write-up on how to run your program, since I may run them. If your program does not run, tell me why—the quality of your analysis will determine how much partial credit you get. In any case, tell which control strategy or strategies you selected and explain why you chose it/them.

Be sure to point out any interesting or neat features of your programs, and discuss any problems you had, ways you overcame them, etc.

Good luck! This is really not hard, at least it shouldn’t be. However, start early!!! In the past, students have found this to be more time-consuming than they expected. Don’t wait till the very last minute, or I can guarantee you won’t get it done on time.

By this time of the semester, I usually notice some problems in one or more students’ Lisp coding, so let me mention them here, so you can avoid them in this assignment. They mostly fall under the heading of “Let Lisp Help You, and Don’t Fight It”. If you fight it, it will usually win.

Use one of these axiom sets for the first part of the assignment, and then come up with one of your own for the second part. Remember: You can convert to CNF before you give the axioms to the program if you like.