Theorem
(Figure 3.5) performs goal reduction.
match
(Figure 3.11) determines if a constant and a
pattern match.
unify
(Figure 3.12) performs a general substitution
so that two expressions can be unified.
disagreement
(Figure 3.13) compares two expressions
to find the first point where they differ.
Theorem
is based on the propositional
calculus, while match
, unify
,
disagreement
supply critical elements to extend
Theorem
to the predicate calculus.Chapter 4 suggests how search strategies can help drive applications, such as theorem proving.
In this project, you are to write a theorem prover for one of these
approaches. With either option, procedure Theorem
should
retain the same interface as the procedure in the text. Thus,
Theorem
will have two parameters: a desired conclusion and
a list of rules or axioms.
Theorem
in the book, your
work should include the following:
Theorem
to expressions in the predicate calculus
(code for exercise 3.12),
Theorem
to utilize a generic depth-first search
(exercise 4.3).
Altogether, this approach should yield a search-based procedure
Theorem
that will prove theorems based on (possibly-recursive)
Horn clauses. If the result does not follow logically from the axioms, the
theorem should report that fact.
If desired (for extra credit), procedure Theorem
might print
out the steps involved in the proof.
(and B_{1} B_{2} ... B_{n})
(not symbol)
, or
(or C_{1} C_{2} ... C_{m})
C_{j}
may be a free symbol or a
constant symbol (const symbol)
or a skolemization function
(func symbol variable-parameters)
In your work, you may use any relevant parts of the programs in ~walker/261/labs/cnf.lsp which take any well-formed formula in the propositional calculus and place it in conjunctive normal form. (Only minor modifications would be needed to expand these procedures to include Skolemization constants and functions.)
Altogether, this approach should yield a procedure Theorem
that takes a conclusion and a list of axioms, such as your answers for the
homework based on the resolution handout, and indicates either that the
result is provable or that no proof is possible.
If desired (for extra credit), procedure Theorem
might print
out the steps involved in the proof.
Final work for this project should be submitted in both written and electronic form. Written work should follow the format specified for Submitting Programs For This Course. An electronic copy of the final version of your program should be sent in ASCII format via e-mail to walker@math.grin.edu before class on Wednesday, March 4.
This document is available on the World Wide Web as
http://www.math.grin.edu/~walker/courses/261/proj-proof.html