John McCarthy's theorem prover

John McCarthy, the inventor of Lisp, died last month.  The new R7RS Scheme standard will be dedicated to his memory.  As another dedication, I thought I'd resurrect his theorem prover, which was published in the Lisp 1.5 manual, and translate it into Scheme. Comments in square brackets are mine; everything else is McCarthy's.

When this code was written, I was still in diapers and a lot of you probably didn't even exist — and yet it only needed indentation, a few changes from cond to if (which helped with the indentation), and a sprinkling of question marks. It's interesting that this Lisp is so old that () is not identical to #f. The procedure names suck and should be replaced with better names (ending in question marks).

;;; We define a function "(theorem s)" whose value is truth
;;; or falsity according to whether the sequent "s" is a theorem.
;;; A sequent is represented by the following S-expression:
;;;     (arrow (term term ...) (term term ...))
;;; Atomic propositional formulae are represented as symbols.
;;; Other propositional formulae are represented as lists whose
;;; first symbols are "not", "and", "or", "implies", or "equiv".
;;; Example: (arrow (and (not p) (not q))) (equiv p q) (or r s))).

;;; The procedure "theorem" is given in terms of auxiliary
;;; functions as follows:

(define (theorem s) (th1 '() '() (cadr s) (caddr s)))

(define (th1 a1 a2 a c)
  (if (null? a)
      (th2 a1 a2 '() '() c)
      (or (member? (car a) c)
          (if (atom? (car a)
                     (th1 (if (member? (car a) a1) a1
                              (cons (car a) a1)) a2 (cdr a) c))
              (th1 a1 (if (member? (car a) a2) a2
                          (cons (car a) a2)) (cdr a) c)))))

(define (th2 a1 a2 c1 c2 c)
  (cond
   ((null? c) (th a1 a2 c1 c2))
   ((atom? (car c)) (th2 a1 a2 (if (member? (car c) c1)
                                   c1
                                   (cons (car c) c1))) c2 (cdr c))
   (else (th2 a1 a2 c1
              (if (member?
                   (car c) c2) c2 (cons (car c) c2))
              (cdr c)))))

(define (th a1 a2 c1 c2)
  (if
   (null? a2) (and (not (null? c2))
                   (thr (car c2) a1 a2 c1 (cdr c2)))
   (thl (car a2) c1 (cdr a2) c1 c2)))

;;; "th" is the main predicate through which all the recursions
;;; take place.  "theorem", "th1", and "th2" break up and sort
;;; the information in the sequent for the benefit of "th".
;;; The fourarguments of "th" are:
;;;     a1: atomic formulae on left side of arrow
;;;     a2: other formulae on left side of arrow
;;;     c1: atomic formulae on right side of arrow
;;;     c1: other formulae on right side of arrow

;;; The atomic formulae are kept separate from the others in
;;; order to make faster the detection of the occurrence of
;;;  formulae on both sides of the arrow and the finding of
;;; the next formulato reduce.  Each use of "th" represents
;;; one reduction according to one of the 10 rules.
;;; The formula to be reduced is chosen from the left side
;;; of the arrow if possible.  According to whether the
;;; formula to be reduced is on the left or the right we use
;;; "thl" or "thr".  We have:

(define (thl u a1 a2 c1 c2)
  (case (car u)
    ((not) (th1r (cadr u) a1 a2 c1 c2))
    ((and) (th2l (cdr u) a1 a2 c1 c2))
    ((or) (and (th1l (cadr u) a1 a2 c1 c2)
               (th1l (caddr u) a1 a2 c1 c2)))
    ((implies) (and (th1l (caddr u) a1 a2 c1
                          c2) (th1r (cadr u) a1 a2 c1 c2)))
    ((equiv) (and (th2l (cdr u) a1 a2 c1 c2)
                  (th2r (cdr u) a1 a2 c1 c2)))
    (else (error "thl: unknown operator" u a1 a2 c1 c2))))

(define (thr u a1 a2 c1 c2)
  (case (car u)
    ((not) (th1l (cadr u) a1 a2 c1 c2))
    ((and) (and (th1r (cadr u) a1 a2 c1 c2)
                (th1r (caddr u) a1 a2 c1 c2)))
    ((or) (th2r (cdr u) a1 a2 c1 c2))
    ((equiv) (and (th11 (cadr u) (caddr u) a1 a2 c1 c2)
                  (th11 (caddr u) (cadr u) a1 a2 c1 c2)))
    (else (error "thr: unknown operator" u a1 a2 c1 c2))))

;;; The functions "th1l", "th1r", "th2l", "th2r", "th11"
;;; distribute the parts of the reduced formula to the
;;; appropriate places in the reduced sequent.
;;; These functions are:

(define (th1l v a1 a2 c1 c2)
  (if
   (atom? v) (or (member? v c1)
                 (th (cons v a1) a2 c1 c2))
   (or (member? v c2) (th a1 (cons v a2) c1 c2))))

(define (th1r v a1 a2 c1 c2)
  (if
   (atom? v) (or (member? v a1)
                 (th a1 a2 (cons v c1) c2))
   (or (member? v c2) (th a1 (cons v a2) c1 c2))))

(define (th2l v a1 a2 c1 c2)
  (cond
   ((atom? (car v)) (or (member? (car v) c1)
                        (th1l (cadr v) (cons (car v) a1) a2 c1 c2)))
   (else (or (member? (car v) c2) (th1l (cadr v) a1 (cons (car v)
                                                          a2) c1 c2)))))

(define (th2r v a1 a2 c1 c2)
  (if
   (atom? (car v)) (or (member? (car v) a1)
                       (th1r (cadr v) a1 a2 (cons (car v) c1) c2))
   (or (member? (car v) a2) (th1r (cadr v) a1 a2 c1
                                       (cons (car v) c2)))))

(define (th11 v1 v2 a1 a2 c1 c2)
  (cond
   ((atom? v1) (or (member? v1 c1) (th1r v2 (cons v1 a1) a2 c1 c2)))
   (else (or (member? v1 c2) (th1r v2 a1 (cons v1 a2) c1 c2)))))

;;; Finally, the function "member?" is defined by

(define (member? x u)
  (or (and (not (null? u))
           (equal? x (car u))) (member? x (cdr u))))

;;; [Note: This function is not the same as "member", because
;;; it returns #t rather than a tail of the list on success.
;;; The "atom?" function is defined as in Lisp 1.5.]

(define (atom? x) (not (pair? x)))

;;; Example:  (theorem '(arrow (p) (or p q))) => #t
;;; because given p, we can infer p v q.