-*- mode:Text -*-
Copyright 1992 Patrick H. Winston.  All rights reserved.
Version 1.1, transferred from master disk on 21 Jan 93
 
This file may reference other files containing copyrighted software.
Any restrictions on the use of such software are described in the
files containing that software.  This file may be freely copied as
long as this notice is kept intact.

PURPOSE

Provides program support program support for Chapter 13, Logic
and Resolution Proof.  Illustrates theorem proving using birds
and blocks.

REMARKS

The resolution theorem prover provided assumes that all
expressions have been converted already to clause form.  See the
resolve.exp file for examples illustrating the required format.

Also, the breadth-first strategy is used for picking clauses to
resolve.  You will be horrified at the number of clauses produced
on one of the sample problems.

PERFORMANCE EXPERIMENT 1

Examine the file resolve.exp.  Run the search experiments by
typing the following command to your lisp system:

(load "resolve.exp")

Alternatively, evaluate each Lisp expression in the file one at a
time, noting what each does.  Be horrified.

PERFORMANCE EXPERIMENT 2

Run the resolution theorem prover with other axiom sets.

SMALL-SCALE LISP PROJECT

Modify the program so that no duplicate clauses are kept.

MEDIUM-SCALE LISP PROJECT

Implement alternative strategies for controlling resolution such
as unit preference and set-of-support.

LARGE-SCALE LISP PROJECT

Implement the necessary machinery to convert a list of axioms and
a theorem into clause form.