Due date now revised to 5pm on Thursday, 2 March.
This assignment is due at 5pm on Thursday, 24 February.
For this assignment, you will build a resolution theorem prover and experiment with it.
A resolution theorem prover consists of several components
Notice that your code does not need to handle equality (=).
You should already have a suitable unification matcher, from assignment 1. If your matcher has problems (or you suspect it may have problems), here's mine.
Scheme gives you several options for packaging several items into one bundle.
Lists are the easiest to construct. However, if data structures are made using only lists, then all parts of the data structure look alike. Scheme's run-time type checking then detects many common errors late, long after the place where the bug lies, and generates uninformative error messages. Occasional use of vectors can improve this situation, because vectors and lists differ in type.
A more powerful approach, however, is to use records. A "record" is the scheme analog of a C struct, a primitive cousin of a Java or C++ class. The functions for manipulating each type of record check that they have been applied to an object of that record type. Therefore, if key data structures are defined as records, the run-time type checking catches many coding errors quickly and generates informative error messages.
Quick overviews of Lisp and Scheme tend to encourage the impression that everything is built with lists and there is no type checking. While many things are built with lists and type checking is quite loose, all reasonable implementations of Lisp/Scheme have something analogous to classes or records.
Here is the declaration of a record type person with three data fields: last, first, and ssn.
;;; Info on a person
(define-record-type person :person
(make-person first last ssn) ;; the function for making a person
person? ;; test if an object is a person
(first get-first set-first!) ;; get and set values of the first field
(last get-last set-last!) ;; get and set values of the last field
(ssn get-ssn set-ssn!)) ;; get and set values of the ssn field
;;; By default, a person just prints as #{Person}. The following piece
;;; of magic causes the printed representation to include the first and
;;; last names.
(define-record-discloser :person
(lambda (s)
`(state ,(list (get-first s) (get-last s)))))
;;; Using the new record type
> (define foo (make-person "margaret" "fleck" 734))
> foo
'#{State ("margaret" "fleck")}
> (get-ssn foo)
734
> (set-first! foo "george")
> foo
'#{State ("george" "fleck")}
> (person? foo)
#t
> (person? 'rock)
#f
>
There are more details in the Scheme48 extensions handout. The format for record declarations is kludgy. Copy-code from the examples and ask Fleck for help if you get stuck.
The theorem prover should take two inputs: a list of facts and a goal to be proved. It might take other inputs such as a bound on the number of iterations, choice of search policy, etc. The goal and each fact in the list should be in scheme-like FOPC format. For example:
'(forall ?x (implies (and (canned ?x) (vegetable ?x))
(goes-in ?x bottom-shelf)))
In this format, the FOPC operators are the symbols 'and, 'or, 'not, 'implies, 'iff, 'forall, and 'exists. 'not takes one input. 'implies, 'iff, 'and, and 'or take exactly two inputs. (Accepting sentences in which 'or and 'and take other numbers of inputs is a possible, but not necessary, extension.)
Variables are symbols whose names start with ?. Constants are numbers and symbols whose names don't start with ?. Predicates and symbols are symbols whose whose names don't start with ?. Symbols with capital letters in their names should not be used because they interfere with my renaming code. (It requires some scheme hackery to create such symbols; you can't just create them by accident.)
Predicates and functions can take any number of inputs, including zero.
Quantifer expressions have the form (quantifier ?myvar expression). For example (forall ?myvar (inside A B)).
The first step in the resolution algorithm is to convert input sentences to conjunctive normal form (CNF). The conversion procedure described in class (or in the book) is a hybrid for use both by hand and when manipulating computer data structures. If we strip the parts that aren't relevant to a computer data structure (e.g. because they are fully parenthesized), the procedure is as follows:
Then, for each sentence you've created:
The file dumb-normalize.scm contains
When you look at my code, you'll see why you should be glad you don't have to write Skolemization and variable renaming. You need to supply code for the other conversion steps.
The file resolution-examples contains a variety of inputs for testing your conversion function.
You will need a function that applies resolution. This function should take two sentences as input. It should
Notice that a pair of sentences may unify in two different ways. So your output will be a list of sentences (perhaps the empty list).
You will need a simple database for storing sentences (in CNF), as you search for resolution proofs. With each sentence, you should store the sentences from which it was derived (i.e. by resolution). Use some sensible special value if the sentence has no ancestors (e.g. was in the original input to the theorem prover). Let's call this package a "state" and encapsulate it using a record with two fields: sentence and ancestors.
Here's a possible declaration for the state record. Because the internal details of a state are complex, it would be cumbersome to see every detail each time a state is displayed.
;;; A state consists of a sentence, plus ancestor states.
(define-record-type state :state
(make-state x y) ;; the function for making a state object
state? ;; test if an object is a state
(x get-sentence set-sentence!) ;; get and set values of the sentence field
(y get-ancestors set-ancestors!)) ;; get and set values of the ancestors field
;;; By default, a state just prints as #{State}. This piece of
;;; magic causes the printed representation to include the sentence
;;; (but not the ancestry details) of the state.
(define-record-discloser :state
(lambda (s)
`(state ,(get-literals (get-sentence s)))))
Initially, your database can simply be a list of states. You may wish to change to a more efficient data structure after you get the basic code working.
Write functions to display the contents of a database, to add states, and to determine whether a state is already in the database. For a list database, you don't really need an add function: just use cons.
Searching the database for a state is slightly more complicated than you might initially think. There might be a state in the database containing a literal copy of the sentence you are searching for. More likely, however, there may be a version of the sentence which is the same except for the variable names.
So you need a function that compares two sentences, but allows a substitution of variable names between the two sentences. Notice that this is not unification. In this case, a variable can only match another variable, not a larger piece of structure. And a variable from one sentence can only be matched to one other variable from the other sentence, not to multiple variables as in unification. So the function you need to write is much simpler than your unification code from assignment 1.
Finally, you need to write a search engine that searches for proofs using resolution. Its inputs should include a list of FOPC sentences (the background facts) and a goal sentence to be proved. See resolution-examples for some examples. Some outputs from my program are in resolution-outputs. (Your output need not be identical, but this will illustrate what correct output looks like.)
A simple search algorithm might have two data structures: a database of facts and a queue of sentences to be examined. The items in both the database and the queue should be states. I recommend using the set-of-support method to guide search. That is, the initial database should contain all the input background facts and the initial queue should contain only the negative of the goal sentence.
The search algorithm then removes the first item from the queue. It is compared to each sentence in the database, to find all possible resolutions. Each resolution will generate a new sentence: add all these sentences to the queue. The search ends when some resolution generates an empty sentence (no literals).
I strongly recommend giving the program an upper bound (e.g. as an input parameter) on the number of queue items it will process. If the theorem prover is getting lost, this will cause it to halt rather than going into an infinite (or very long) loop. Use ctrl-C to halt infinite loops.
When the search algorithm has finished, return the final sentence which contained no literals. By tracing backwards from the ancestors of the sentence, you should be able to print the resolution proof as the final step in your program.
Once you have one version of the theorem prover working, try adding various extensions and options. Experiment with how they affect performance.
This code is much easier to debug if you use some record types. The above directions recommend using two record types: sentence and state. You don't have to follow this recipe exactly. However, I strongly recommend not implementing all your data structures with lists of lists of lists. A few strategically placed record types will result in much more meaningful error messages.
Our scheme binary contains a hash table facility. See the Scheme48 extensions handout.
The Scheme48 extensions handout describes functions for removing items from a list and for removing duplicates from a list. However, these two functions seem use eq? to compare items. This isn't right for your resolution program: two similar-looking lists created independently will be equal? but not eq? Here are some similar functions using equal?
(define (remove item items) (cond ((null? items) '()) ((equal? item (car items)) (remove item (cdr items))) (#t (cons (car items) (remove item (cdr items)))))) (define (remove-duplicates-equal items) (cond ((null? items) '()) ((member (car items) (cdr items)) (remove-duplicates (cdr items))) (#t (cons (car items) (remove-duplicates-equal (cdr items))))))
Examine both versions of the unique ID generator in dumb-normalize.scm. This code creates the scheme analog of a C(++) static variable, i.e. a variable whose value persists from call to call. To do this, we use an alternative version of the define form, in which the function name is bare (no parens around it) and the value assigned to it is a lambda expression.
The static variable counter is declared outside this lambda expression. Counter is private to the ID functions, because only the code for the ID functions lives inside the scope of the let defining counter. However, because counter is not actually defined inside the ID function's lambda expression, it persists from call to call rather than being created anew.
If you type into the interpreter an expression whose parentheses are not all closed, and then hit enter, it sometimes looks as though scheme is running but in an infinite loop. Type one or more close parentheses followed by enter, to see if this is your problem.
When a function is processing an expression that takes a variable number of inputs (e.g. predicates, functions), the scheme operator map is very useful for calling the function recursively on all of the inputs.
As for the previous assignments, you should turn in a hardcopy of your code and a separate written description of what your code does and how it works, and also submit a copy of your code using cs151submit.
In your description, be sure to include some sample inputs and outputs, a description of which features your program implemented, and an analysis of how performance was affected by different search strategies and optimization features.
This page is maintained by Margaret Fleck.