# Project on Automated Proof

Draft Project Due: Monday, March 2 (written version only)
Final Project Due: Wednesday, March 4 (both written and e-mail copies)

### Introduction

Chapter 3 presents several elements of an automated theorem-prover:
• Procedure `Theorem` (Figure 3.5) performs goal reduction.
• Axioms are written as Horn clauses in the propositional calculus,
• Inference proceeds linearly through the rules, using backwards chaining,
• rules are assumed to be non-recursive.
• Procedure `match` (Figure 3.11) determines if a constant and a pattern match.
• Procedure `unify` (Figure 3.12) performs a general substitution so that two expressions can be unified.
• Procedure `disagreement` (Figure 3.13) compares two expressions to find the first point where they differ.
As noted in the text, `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.

### Project Overview

In this project, you are to write a theorem-prover for expressions in the predicate calculus. Theorems may be written in either of two forms:
1. Theorems may be written as a sequence of Horn clauses in the predicate calculus, or
2. Theorems may be written as axioms in conjunctive normal form, with the theorem's conclusion negated.
In the first case, proof proceeds by goal reduction (with backward chaining); in the second case, proof proceeds by resolution and unification until a contradiction is obtained.

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.

### Project Details

1. If you choose to extend procedure `Theorem` in the book, your work should include the following:
1. Allow recursive axioms (exercise 3.6),
2. Extend `Theorem` to expressions in the predicate calculus (code for exercise 3.12),
3. Reimplement `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.

4. If you choose to write a theorem prover, based on axioms in conjunctive normal form, you should base a solution on the following:
1. assume axioms are given in conjunctive normal form according to the syntax,
• an axiom has the form ``` (and B1 B2 ... Bn)```
• where each Bi has the form symbol, `(not symbol)`, or `(or C1 C2 ... Cm)`
• and where each symbol or `Cj` may be a free symbol or a constant symbol `(const symbol)` or a skolemization function `(func symbol variable-parameters)`
2. assume the conclusion is given in positive form (so it will have to be negated before proof can begin).
3. assume skolemization has already been performed for the given axioms and the conclusion.

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.

### Submitting Programs For This Project:

A preliminary hard-copy version of your program should be turned in at class on Monday, March 2, and should include your code and either your test runs or a written status report on what remains to be done to complete your program.

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
```

created February 22, 1998
last revised February 22, 1998