8. A COMPLETE LISP PROGRAM - THE WANG ALGORITHM FOR THE PROPOSITIONAL CALCULUS

This section gives an example of a complete collection of LISP function definitions which were written to define an algorithm. The program was then run on several test cases. The algorithm itself is explained, and is then written in M-expressions. The complete input card deck and the printed output of the run are reprinted here.

The Wang Algorithm^8.1 is a method of deciding whether or not a formula in the prepositional calculus is a theorem. The reader will need to know something about the prepositional calculus in order to understand this discussion.

We quote from pages 5 and 6 of Wang's paper:

"The prepositional calculus (System P)

Since we are concerned with practical feasibility, it is preferable to use more logical connectives to begin with when we wish actually to apply the procedure to concrete cases. For this purpose we use the five usual logical constants $\sim$ (not), $\&$ (conjunction), $\lor$ (disjunction), $\supset$ (implication), $\equiv$ (biconditional), with their usual interpretations.

"A prepositional letter P, Q, R, M or N, et cetera, is a formula (and an "atomic formula"). If $\phi , \psi$ are formulae, then $\sim \phi , \phi \& \psi , \phi \lor \psi , \phi \supset \psi , \phi \equiv \psi$ are formulae. If $\pi , \rho$ are strings of formulae (each, in particular, might be an empty string or a single formula) and $\phi$ is a formula, then $\pi , \phi , \rho$ is a string and $\pi \rightarrow \rho$ is a sequent which, intuitively speaking, is true if and only if either some formula in the string $\pi$ (the "antecedent") is false or some formula in the string $\rho$ (the "consequent") is true, i.e., the conjunction of all formulae in the antecedent implies the disjunction of all formulae in the consequent.

"There are eleven rules of derivation. An initial rule states that a sequent with only atomic formulae (proposition letters) is a theorem if and only if a same formula occurs on both sides of the arrow. There are two rules for each of the five truth functions - one introducing it into the antecedent, one introducing it into the consequent. One need only reflect on the intuitive meaning of the truth functions and the arrow sign to be convinced that these rules are indeed correct. Later on, a proof will be given of their completeness, i.e., all intuitively valid sequents are provable, and of their consistency, i.e., all provable sequents are intuitively valid.

"Pl. Initial rule: if $\lambda, \zeta$ are strings of atomic formulae, then $\lambda \rightarrow \zeta$ is a theorem if some atomic formula occurs on both sides of the arrow.

"In the ten rules listed below, $\lambda$ and $\zeta$ are always strings (possibly empty) of atomic formulae. As a proof procedure in the usual sense, each proof begins with a finite set of cases of Pl and continues with successive consequences obtained by the other rules."

"As will be explained below, a proof looks like a tree structure growing in the wrong direction. We shall, however, be chiefly interested in doing the step backwards, thereby incorporating the process of searching for a proof.

"The rules are so designed that given any sequent, we can find the first logical connective, and apply the appropriate rule to eliminate it, thereby resulting in one or two premises which, taken together, are equivalent to the conclusion. This process can be repeated until we reach a finite set of sequents with atomic formulae only. Each connective-free sequent can then be tested for being a theorem or not, by the initial rule. If all of them are theorems, then the original sequent is a theorem and we obtain a proof; otherwise we get a counter example and a disproof. Some simple samples will make this clear.

"For example, given any theorem of "Principia," we can automatically prefix an arrow to it and apply the rules to look for a proof. When the main connective is $\supset$, it is simpler, though not necessary, to replace the main connective by an arrow and proceed. For example:

*2.45. $\vdash : \sim (P\lor Q) . \supset . \sim P$, 
*5.21. $\vdash : \sim P \& \sim Q . \supset . P \equiv Q$

can be rewritten and proved as follows:

*2.45. $\sim (P\lor Q) \rightarrow \sim P$        (1) $\rightarrow \sim P, P \lor Q$        (2) $P \rightarrow P \lor Q$        (3) $P \rightarrow P, Q$         VALID 
 
*5.21. $\rightarrow \sim P \& \sim Q . \supset . P \equiv Q$        (1) $\sim P \& \sim Q \rightarrow P \equiv Q$        (2) $\sim P, \sim Q \rightarrow P \equiv Q$        (3) $\sim Q \rightarrow P \equiv Q, P$        (4) $\rightarrow P \equiv Q, P, Q$        (5) $P \rightarrow Q, P, Q$         VALID 
        (5) $Q \rightarrow P, P, Q$         VALID 
 
P2a. Rule $\rightarrow \sim : If \phi ,\zeta \rightarrow \lambda,\rho then \zeta \rightarrow \lambda, \sim \phi , \rho .$P2b. Rule $\sim \rightarrow : If \lambda,\rho \rightarrow \pi ,\phi then \lambda, \sim \phi , \rho \rightarrow \pi .$P3a. Rule $\rightarrow \& : If \zeta \rightarrow \lambda,\phi ,\rho and \zeta \rightarrow \lambda,\psi ,\rho then \zeta \rightarrow \lambda, \phi \&\psi , \rho .$P3b. Rule $\& \rightarrow : If \lambda,\phi ,\psi ,\rho \rightarrow \pi then \lambda, \phi \&\psi , \rho \rightarrow \pi .$P4a. Rule $\rightarrow \lor : If \zeta \rightarrow \lambda,\phi ,\psi ,\rho then \zeta \rightarrow \lambda, \phi \lor \psi , \rho .$P4b. Rule $\lor \rightarrow : If \lambda,\phi ,\rho \rightarrow \pi and \lambda,\psi ,\rho \rightarrow \pi then \lambda, \phi \lor \psi , \rho \rightarrow \pi .$P5a. Rule $\rightarrow \supset : If \zeta ,\phi \rightarrow \lambda,\psi ,\rho then \zeta \rightarrow \lambda, \phi \supset \psi , \rho .$P5b. Rule $\supset \rightarrow : If \lambda,\psi ,\rho \rightarrow \pi and \lambda,\rho \rightarrow \pi ,\phi then \lambda, \phi \supset \psi , \rho \rightarrow \pi .$P6a. Rule $\rightarrow \equiv : If \phi ,\zeta \rightarrow \lambda,\psi ,\rho and \psi ,\z... ...ow \lambda,\phi ,\rho then \zeta \rightarrow \lambda, \phi \equiv \psi , \rho .$P6b. Rule $\equiv \rightarrow : If \phi ,\psi ,\lambda,\rho \rightarrow \pi and \lambda,\r... ...htarrow \pi ,\phi ,\psi then \lambda, \phi \equiv \psi , \rho \rightarrow \pi .$

(2) The LISP Program. We define a function theorem[s] whose value is truth or falsity according to whether the sequent s is theorem.

The sequent

$s: \phi _{1}, \ldots , \phi _{n} \rightarrow \psi _{1}, \ldots , \psi _{m}$

is represented by the S-expression

$s^{*}$: (ARROW, ( $\phi _{1}^{*}, \ldots , \phi _{n}^{*}), (\psi _{1}^{*}, \ldots , \psi _{n}^{*}$))

where in each case the ellipsis ...denotes missing terms, and where $\phi ^{*}$ denotes the S-expression for $\phi$.

Propositional formulae are represented as follows:

1. For "atomic formulae" (Wang's terminology) we use "atomic symbols" (LISP terminology).

2. The following table gives our "Cambridge Polish" way of representing prepositional formulae with given main connectives.

1. $\sim \phi$ becomes (NOT $\phi ^{*}$) 
2. $\phi \& \psi$ becomes (AND $\phi ^{*} \psi ^{*}$) 
3. $\phi \lor \psi$ becomes (OR $\phi ^{*} \psi ^{*}$) 
4. $\phi \supset \psi$ becomes (IMPLIES $\phi ^{*} \psi ^{*}$) 
5. $\phi \equiv \psi$ becomes (EQUIV $\phi ^{*} \psi ^{*}$)

Thus the sequent

$\sim P \& \sim Q \rightarrow P \equiv Q, R \lor S$

is represented by

(ARROW ((AND (NOT P) (NOT Q))) ((EQUIV P Q) (OR R S)))

The S-function theorem[s] is given in terms of auxiliary functions as follows:

theorem[s] = thl[NIL;NIL;cadr[s];caddr[s]] 
 
th1[a1;a2;a;c] = [null[a] $\rightarrow$ th2[a1;a2;NIL;NIL;c];T $\rightarrow$        member[car[a];c] $\lor$ [atom [car [a]] $\rightarrow$        thl[[member[car[a];a1] $\rightarrow$ a1; 
        T $\rightarrow$ cons[car[a];a1]];a2;cdr[a];c];T $\rightarrow$ thl[a1;[ 
        member[car[a];a2] $\rightarrow$ a2;T $\rightarrow$ cons[ 
        car[a];a2]];cdr[a];c]]] 
th2[a1;a2;c1;c2;c] = [null[c] $\rightarrow$ th[a1;a2;c1;c2];atom[ 
        car[c]] $\rightarrow$ th2[a1;a2;[member[car[ 
        c];c1] $\rightarrow$ c1; T $\rightarrow$ cons[car[c];c1]]; 
        c2;cdr[c]];T $\rightarrow$ th2[a1;a2;c1;[ 
        member[car[c];c2] $\rightarrow$ c2;T $\rightarrow$ cons[ 
        car[c];c2]];cdr[c]]] 
th[a1;a2;c1;c2] = [null[a2] $\rightarrow$ $\sim$null[c2] $\land$ thr[car[c2]; 
        a1;a2;c1;cdr[c2]];T $\rightarrow$ thl[car[a2]; 
        a1;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 four arguments 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 c2: 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 formula on both sides of the arrow and the finding of the next formula to reduce. Each use of th represents one reduction according to one of the 10 rules. The forumla 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 right we use thl or thr. We have

thl[u;a1;a2;c1;c2] = [ 
        car[u] = NOT $\rightarrow$ th1r[cadr[u];a1;a2;c1;c2]; 
        car[u] = AND $\rightarrow$ th2l[cdr[u];a1;a2;c1;c2]; 
        car[u] = OR $\rightarrow$ th1l[cadr[u];a1;a2;c1;c2] $\land$ th1l 
                caddr[u];a1;a2;c1;c2]; 
        car[u] = IMPLIES $\rightarrow$ th1l[caddr[u];a1 ;a2;c1;c2] $\land$ th1r 
                cadr[u];a1;a2;c1;c2]; 
        car[u] = EQUIV $\rightarrow$ th2l[cdr[u];a1;a2;c1;c2] $\land$ th2r 
                cdr[u];a1;a2;c1;c2]; 
        T $\rightarrow$ error[list[THL;u;a1;a2;c1;c2]]] 
 
thr[u;a1;a2;c1;c2] = [ 
        car[u] = NOT $\rightarrow$ th1l[cadr[u];a1;a2;c1;c2]; 
        car[u] = AND $\rightarrow$ th1r[cadr[u];a1;a2;c1;c2] $\land$ th1r 
                caddr[u];a1;a2;c1;c2]; 
        car[u] = OR $\rightarrow$ th2r[cdr[u];a1;a2;c1;c2]; 
        car[u] = IMPLIES $\rightarrow$ th11[cadr[u];caddr[u];a1;a2;c1;c2]; 
        car[u] = EQUIV $\rightarrow$ th11[cadr[u];caddr[u];a1;a2;c1;c2] $\land$                th11[caddr[u];cadr[u];a1;a2;c1;c2]; 
        T $\rightarrow$ error[THR;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

th1l[v;a1;a2;c1;c2] = [atom[v] $\rightarrow$ member[v;c1] $\lor$        th[cons[v;a1];a1;c1;c2];T $\rightarrow$ member[v;c2] $\lor$        th[a1;cons[v;a2];c1;c2]] 
 
th1r[v;a1;a2;c1;c2] = [atom[v] $\rightarrow$ member[v;a1] $\lor$        th[a1;a2;cons[v;c1];c2];T $\rightarrow$ member[v;a2] $\lor$        th[a1;a2;c1;cons[v;c2]]] 
 
th2l[v;a1;a2;c1;c2] = [atom[car[v]] $\rightarrow$ member[car[v];c1] $\lor$        th1l[cadr[v];cons[car[v];a1];a2;c1;c2];T $\rightarrow$ member[ 
                car[v];c2] $\lor$        th1l[cadr[v];a1;cons[car[v];a2];c1;c2]] 
 
th2r[v;a1;a2;c1;c2] = [atom[car[v]] $\rightarrow$ member[car[v];a1] $\lor$        th1r[cadr[v];a1;a2;cons[car[v];c1];c2];T $\rightarrow$ member [ 
                car[v];a2] $\lor$        th1r[cadr[v];a1;a2;c1;cons [car [v];c2]]] 
 
th1l[v1;v2;a1;a2;c1;c2] = [atom[v1] $\rightarrow$ member[v1;c1] $\lor$        thlr[v2;cons[v1;a1];a2;c1;c2];T $\rightarrow$ member[v1;c2] $\lor$        th1r[v2;a1;cons[v1;a2];cl ;c2]]

Finally the function member is defined by

member[x;u] = $\sim$ null[u] $\land$ [equal[x;car[u]] $\lor$member[x;cdr[u]]]

The entire card deck is reprinted below, with only the two loader cards, which are binary, omitted. The function member is not defined because it is already in the system.

* M948-1207 LEVIN, LISP, TEST, 2,3,250,0 
        TEST WANG ALGORITHM FOR THE PROPOSITIONAL CALCULUS 
 
DEFINE (( 
(THEOREM (LAMBDA (S) (TH1 NIL NIL (CADR S) (CADDR S)))) 
 
(TH1 (LAMBDA (A1 A2 A C) (COND ((NULL A) 
        (TH2 A1 A2 NIL NIL C)) (T 
        (OR (MEMBER (CAR A) C) (COND ((ATOM (CAR A)) 
        (TH1 (COND ((MEMBER (CAR A) A1) A1) 
        (T (CONS (CAR A) A1))) A2 (CDR A) C)) 
        (T (TH1 A1 (COND ((MEMBER (CAR A) A2) A2) 
        (T (CONS (CAR A) A2))) (CDR A) C)))))))) 
 
(TH2 (LAMBDA (A1 A2 C1 C2 C) (COND 
        ((NULL C) (TH A1 A2 C1 C2)) 
        ((ATOM (CAR C)) (TH2 A1 A2 (COND 
        ((MEMBER (CAR C) C1) C1) (T 
        (CONS (CAR C) C1))) C2 (CDR C))) 
        (T (TH2 A1 A2 C1 (COND ((MEMBER 
        (CAR C) C2) C2) (T (CONS (CAR C) C2))) 
        (CDR C)))))) 
 
(TH (LAMBDA (A1 A2 C1 C2) (COND ((NULL A2) (AND (NOT (NULL C2)) 
        (THR (CAR C2) A1 A2 C1 (CDR C2)))) (T (THL (CAR A2) A1 (CDR A2) 
        C1 C2))))) 
 
(THL (LAMBDA (U A1 A2 C1 C2) (COND 
        ((EQ (CAR U) (QUOTE NOT)) (TH1R (CADR U) A1 A2 C1 C2)) 
        ((EQ (CAR U) (QUOTE AND)) (TH2L (CDR U) A1 A2 C1 C2)) 
        ((EQ (CAR U) (QUOTE OR)) (AND (TH1L (CADR U) A1 A2 C1 C2) 
        (TH1L (CADDR U) A1 A2 C1 C2) )) 
        ((EQ (CAR U) (QUOTE IMPLIES)) (AND (TH1L (CADDR U) A1 A2 C1 
        C2) (TH1R (CADR U) A1 A2 C1 C2) )) 
        ((EQ (CAR U) (QUOTE EQUIV)) (AND (TH2L (CDR U) A1 A2 C1 C2) 
        (TH2R (CDR U) A1 A2 C1 C2) )) 
        (T (ERROR (LIST (QUOTE THL) U A1 A2 C1 C2))) 
        ))) 
 
(THR (LAMBDA (U A1 A2 C1 C2) (COND 
        ((EQ (CAR U) (QUOTE NOT)) (TH1L (CADR U) A1 A2 C1 C2)) 
        ((EQ (CAR U) (QUOTE AND)) (AND (TH1R (CADR U) A1 A2 C1 C2) 
        (TH1R (CADDR U) A1 A2 C1 C2) )) 
        ((EQ (CAR U) (QUOTE OR)) (TH2R (CDR U) A1 A2 C1 C2)) 
        ((EQ (CAR U) (QUOTE IMPLIES)) (TH11 (CADR U) (CADDR U) 
         A1 A2 C1 C2)) 
        ((EQ (CAR U) (QUOTE EQUIV)) (AND (TH11 (CADR U) (CADDR U) 
        A1 A2 C1 C2) (TH11 (CADDR U) (CADR U) A1 A2 C1 C2) )) 
        (T (ERROR (LIST (QUOTE THR) U A1 A2 C1 C2))) 
        ))) 
 
(TH1L (LAMBDA (V A1 A2 C1 C2) (COND 
        ((ATOM V) (OR (MEMBER V C1) 
        (TH (CONS V A1) A2 C1 C2) )) 
        (T (OR (MEMBER V C2) (TH A1 (CONS V A2) C1 C2) )) 
        ))) 
 
(TH1R (LAMBDA (V A1 A2 C1 C2) (COND 
        ((ATOM V) (OR (MEMBER V A1) 
        (TH A1 A2 (CONS V C1) C2) )) 
        (T (OR (MEMBER V A2) (TH A1 A2 C1 (CONS V C2)))) 
        ))) 
 
(TH2L (LAMBDA (V A1 A2 C1 C2) (COND 
        ((ATOM (CAR V)) (OR (MEMBER (CAR V) C1) 
        (TH1L (CADR V) (CONS (CAR V) A1) A2 C1 C2))) 
        (T (OR (MEMBER (CAR V) C2) (TH1L (CADR V) A1 (CONS (CAR V) 
        A2) C1 C2))) 
        ))) 
 
(TH2R (LAMBDA (V A1 A2 C1 C2) (COND 
        ((ATOM (CAR V)) (OR (MEMBER (CAR V) A1) 
        (TH1R (CADR V) A1 A2 (CONS (CAR V) C1) C2))) 
        (T (OR (MEMBER (CAR V) A2) (TH1R (CADR V) A1 A2 C1 
        (CONS (CAR V) C2)))) 
        ))) 
 
(TH11 (LAMBDA (VI V2 A1 A2 C1 C2) (COND 
        ((ATOM VI) (OR (MEMBER VI C1) (TH1R V2 (CONS VI A1) A2 C1 
        C2))) 
        (T (OR (MEMBER VI C2) (TH1R V2 A1 (CONS VI A2) C1 C2))) 
        ))) 
)) 
 
TRACE ((THEOREM TH1 TH2 TH THL THR TH1L TH1R TH2L TH2R TH11)) 
 
THEOREM 
((ARROW (P) ((OR P Q)))) 
 
UNTRACE ((THEOREM TH1 TH2 THR THL TH1L TH1R TH2L TH2R TH11)) 
 
THEOREM 
((ARROW ((OR A (NOT B))) ((IMPLIES (AND P Q) (EQUIV P Q))) )) 
 
STOP)))    )))     )))     ))) 
        FIN     END OF LISP RUN        M948-1207 LEVIN

This run produced the following output:

* M948-1207 LEVIN, LISP, TEST, 2, 3, 250, 0 
        TEST    WANG ALGORITHM FOR THE PROPOSITIONAL CALCULUS 
THE TIME (8/ 8 1506. 1) HAS COME, THE WALRUS SAID, TO TALK OF MANY THINGS 
...- LEWIS CARROLL - 
 
FUNCTION EVALQUOTE HAS BEEN ENTERED, ARGUMENTS.. 
DEFINE 
[ The complete list of definitions read in is omitted to save space.] 
 
END OF EVALQUOTE. VALUE IS.. 
(THEOREM TH1 TH2 TH THL THR TH1L TH1R TH2L TH2R TH11) 
 
FUNCTION EVALQUOTE HAS BEEN ENTERED, ARGUMENTS.. 
TRACE 
((THEOREM TH1 TH2 TH THL THR TH1L TH1R TH2L TH2R TH11)) 
 
END OF EVALQUOTE, VALUE IS.. 
NIL 
 
FUNCTION EVALQUOTE HAS BEEN ENTERED. ARGUMENTS.. 
THEOREM 
((ARROW (P) ((OR P Q))))