;;;; -*- mode:Lisp; syntax:Common-Lisp; package:user -*- ;;;;
;;;; Copyright 1992 Patrick H. Winston.  All rights reserved.
;;;; Version 1.1.1, transferred from master disk on 23 Apr 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: program support for Chapter 13,
;;;; Logic and Resolution Proof

;;;; REMARKS

#|

Clauses are to be expressed in the following format:

(<number> <first literal>
	  v <second literal>
	  .
	  .
	  .
	  v <final literal>)


Variables in clauses are marked by embedding in a list whose
first element is a question mark and whose second element is the
variable name.  For example, the variable u appears as (? u).

The PROVE procedure expects a list of quoted clauses.

The theorem literal, negated as required for
proof-by-contradiction, appears last in the examples.

|#

;;;; LOAD RESOLUTION THEOREM PROVER
(load "match.lsp")
(load "resolve.lsp")

;;;; RUN EXPERIMENTS

(format t "~%~%Experiment #1---SQUIGS example:")
(prove '(1 (not (feathers squigs)) v (bird squigs))
       '(2 (feathers squigs))
       '(3 (not (bird squigs))))

(format t "~%~%Experiment #2---ABOVE example:")
(prove '(1 (not (on (? u) (? v)))
	   v (above (? u) (? v)))
       '(2 (not (above (? x) (? y)))
	   v (not (above (? y) (? z)))
	   v (above (? x) (? z)))
       '(3 (on b a))
       '(4 (on a table))
       '(5 (not (above b table))))