Theorem Prover

Theorem Prover

In this problem set, we will be using a not so simple Scheme program that proves theorems in the First Order predicate Calculus. The code is a translation into Scheme (and slight extension) of a Common-Lisp prover written by Shaul Markovitch from Technion. It also uses some code for unification and CNF conversion by Peter Norvig.

Loading the file \"load-prover-mit-scheme.scm\", after you set the working directory to the problem set directory loads the appropriate files. To see the system in operation:


(cd ps-directory)
(load "load-prover-mit-scheme.scm")
(test)

This will run the test case in the file \"test1.lgc\" (look at the definition of (test) in the file \"prover.scm\") . It will prove (mother ?mom yzhak) using three different strategies. These strategies differ primarily in the order in which resolutions are done - these strategies are discussed in class. Note that the choice of strategies does make a difference. We have set the strategy to one that generally works well; you can experiment using the compare-strategies function.

The files read by the prover are made up of lists of sentences in the Scheme-like quantified notation. These are converted to clause form by the code that reads them in and the resulting clauses are set to the variable *axioms*. The top-level call to the theorem prover is:


(theorem-prover theorem axioms list-of-ans-vars)

A typical call might be:


(theorem-prover '(mother ?mom yzhak) *axioms* '(?mom))

The variable *resource-limit* [in prover.scm] controls how many resolution steps are attempted before halting. The function print-proof [in prover.scm] takes the output of the theorem prover and tries to print it in a format compatible with the proofs we have seen in our on-line problems. The following will get you going (once you have added axioms to \"blocks.lgc\")


(cd ps-directory)
(load "load-prover-mit-scheme.scm")
(read-axioms "blocks.lgc")
(prove '(on yellow ?b) '(?b))

This will run the prover and print the proof.