Winston & Horn: A Propositional Calculus Resolution Theorem Prover in Lisp

From by Patrick Winston's and Berthold Horn's famous classic on AI and Lisp (1981) - the first edition is available as a PDF here.

Amazon link:(3rd edition)

How to code a resolution theorem prover for the propositional calculus in Lisp (page 232).

---

Resolution is one way to Prove Theorems In Propositional Calculus 

Theorem Proving is a highly developed field that requires considerable mathematical sophistication to understand fully. Still, if we limit ourselves to proofs in the propositional calculus, we can build a simple theorem prover. It will be based on the so-called resolution principle (which can be extended to deal with the more difficult problems of the predicate calculus). The key to this theorem prover, again, is a matcher.

A theorem in the propositional calculus, for our purpose, consists of a premise and a conclusion, both expressed in LISP-like prefix notation. The following sets up a typical premise and conclusion:

(SETQ PREMISE
   '(AND (OR Q (NOT P))
               (OR R (NOT Q))
               (OR S (NOT R))
               (OR (NOT U) (NOT S))))

(SETQ CONCLUSION
   '(AND (OR (NOT P) (NOT U))))

These are examples of conjunctive normal form since only atoms appear inside NOTs, only NOTs or atoms appear inside ORs, and only ORs appear inside ANDs. Each of the OR lists is called a clause. Each atom or atom with a NOT is called a literal.

Our theorem prover will use the assumption that all inputs are in conjunctive normal form because it can be shown that anything written in terms of ANDs, ORs, and NOTs can be placed in equivalent conjunctive normal form.

■ To prove a theorem, it must be shown that the premise implies the conclusion. For a premise to imply a conclusion, it must be that any combination of T and NIL values for the atoms in the premise that make the premise evaluate to T also makes the conclusion evaluate to T. Or said another way, to prove a theorem, it must be shown that any combination of literal values that makes the premise true also makes the conclusion true.

Clearly, theorems can be proved by simply trying all ways to bind the atoms to T and NIL, checking that no combination causes the premise to evaluate to T and the conclusion to NIL. Resolution offers an alternative. We first list the steps involved to give a general feel for what is involved, and then we will explain why they work.

■ Step 1: Negate the conclusion, put it into conjunctive normal form, and combine it with the premise.

In our example, negating the conclusion yields the following:

(AND (OR P) (OR U))

Combining this with the premise produces the following result:

(AND (OR P)
           (OR U)
           (OR Q (NOT P))
           (OR R (NOT Q))
           (OR S (NOT R))
           (OR (NOT U) (NOT S)))

■ Step 2: Search for two clauses in which the same atom appears naked in one and negated in the other. Form a new clause by combining everything in the two clauses except for the naked atom and its negation. The two clauses involved are said to resolve. The new clause is called a resolvent. Combine the resolvent with the other clauses.

For the example, the first and the third clauses resolve, producing a resolvent. That is, (OR P) and (OR Q (NOT P)) yield (OR Q). Combining this with the rest of the clauses yields this:

(AND (OR Q)
           (OR P)
           (OR U)
           (OR Q (NOT P))
           (OR R (NOT Q))
           (OR S (NOT R))
           (OR (NOT U) (NOT S)))

■ Step 3: Repeat step 2 until no two clauses resolve or two clauses resolve to (OR). If no two clauses resolve, report failure. If two resolve to (OR), report success.

The key step clearly is a matching process, the one that produces resolvents of two clauses. The following matching function does the job: 

(DEFUN RESOLVE (X Y)
    (PROG (REST-X REST-Y)
        (SETQ REST-Y (CDR Y))         ; Get rid of OR.
        (SETQ REST-X (CDR X))         ; Get rid of OR.
        LOOP
        (COND ((NULL REST-X) (RETURN 'NO-RESOLVENT))      ; Any atom left to try?
                     ((MEMBER ( INVERT (CAR REST-X)) REST-Y)        ; Is negation in Y?
                      (RETURN (CONS 'OR                                                   ; Add OR.
                                                     (COMBINE (CAR REST-X)           ; Tidy up.
                                                                          (APPEND (CDR X) (CDR Y)))))))
         (SETQ REST-X (CDR REST-X))
        (GO LOOP))) 

Note that two auxiliary functions are needed. INVERT returns a bare atom if the argument is in the form of (NOT <atom>) . It wraps its argument in a NOT if the argument is an atom. COMBINE gets rid of the match-causing atom and its negation and makes sure there are no repeated elements in the resulting clause:

(DEFUN INVERT (X)
               (COND ((ATOM X) (LIST 'NOT X))
                             (T (CADR X)))) 

(DEFUN COMBINE (A L)
               (COND ((NULL L) NIL)
                             ((OR (EQUAL A (CAR L))                                     ; Is it there?
                                      (EQUAL (INVERT A) (CAR L))                   ;  Is negation there?
                                      (MEMBER (CAR L) (CDR L)))                     ; Is it there twice?
                              (COMBINE A (CDR L)))                                       ; Then get rid of it.
                            (T (CONS (CAR L) (COMBINE A (CDR L))))))    ; Otherwise keep it.

The function PROVE consists of nested loops that search for resolvable clauses and add resolvents to the clause list. Here we show it applied to an example: 

(PROVE PREMISE NEGATION)
    (THE CLAUSE (OR Q (NOT P)))
    (AND THE CLAUSE (OR R (NOT Q)))
    (PRODUCE A RESOLVENT: (OR (NOT P) R))
    (THE CLAUSE (OR (NOT P) R))
    (AND THE CLAUSE (OR S (NOT R)))
    (PRODUCE A RESOLVENT: (OR (NOT P) S))
    (THE CLAUSE (OR (NOT P) S))
    (AND THE CLAUSE (OR (NOT U) (NOT S)))
    (PRODUCE A RESOLVENT: (OR (NOT P) (NOT U)))
    (THE CLAUSE (OR (NOT P) (NOT U)))
    (AND THE CLAUSE (OR P))
    (PRODUCE A RESOLVENT: (OR (NOT U)))
    (THE CLAUSE (OR (NOT U)))
    (AND THE CLAUSE (OR U))
    (PRODUCE THE EMPTY RESOLVENT)
    (THEOREM PROVED)

There are, incidentally, many ways to make resolution more efficient by limiting the attempts at resolving clauses. For example, any clause containing an atom and its negation can be ignored. 

(DEFUN PROVE (PREMISE NEGATION)
     (PROG (FIRST REST REMAINDER RESOLVENT CLAUSES)
          (SETQ CLAUSES (APPEND (CDR PREMISE)           ; Purge ANDS
                                                           (CDR NEGATION)))
          FIND-CLAUSE                                                       ; this is a label for 'GO' at end
          (SETQ REMAINDER CLAUSES)
         TRY-NEXT-X-CLAUSE
          (COND ((NULL REMAINDER) (RETURN '(THEOREM NOT PROVED))))
          (SETQ FIRST (CAR REMAINDER))
          (SETQ REST (CDR REMAINDER))
        TRY-NEXT-Y-CLAUSE
         (COND ((NULL REST) (SETQ REMAINDER (CDR REMAINDER))  ; Doesn't resolve.
                                                (GO TRY-NEXT-X-CLAUSE)))
         (SETQ RESOLVENT (RESOLVE FIRST (CAR REST)))                   ; Try resolving.
         (COND ((OR (EQUAL RESOLVENT 'NO-RESOLVENT)
                               (MEMBER RESOLVENT CLAUSES))                          ; Resolvent known.
                        (SETQ REST (CDR REST))
                        (GO TRY-NEXT-Y-CLAUSE))
                       ((NULL (CDR RESOLVENT))                                                ; Resolvent empty.
                        (PRINT (APPEND '(THE CLAUSE) (LIST FIRST)))
                        (PRINT (APPEND '(AND THE CLAUSE) (LIST (CAR REST))))
                        (PRINT '(PRODUCE THE EMPTY RESOLVENT))
                        (RETURN '(THEOREM PROVED)))
                      (T (SETQ CLAUSES (CONS RESOLVENT CLAUSES))         ; Resolvent is new.
                       (PRINT (APPEND '(THE CLAUSE) (LIST FIRST)))
                       (PRINT (APPEND '(AND THE CLAUSE) (LIST (CAR REST))))
                       (PRINT (APPEND '(PRODUCE A RESOLVENT:) (LIST RESOLVENT)))
                       (GO FIND-CLAUSE))))) 

---

I haven't yet tried to copy and paste this code into a Lisp system so there may be the odd parenthesis missing. After checking it out, my next step would be to remove all those confusing loops and write it in a recursive fashion. Also experiment with different control strategies, such as set-of-support.

But Heidi Morkland was way ahead of me.

I do find the archaic style rather attractive (CADR!).

---

Compare this PL resolution prover written in Prolog by Markus Triska in 2006.

Resolution calculus for propositional logic.

   Input is a formula in conjunctive normal form, represented as a
   list of clauses; clauses are lists of atoms and terms not/1.

   Example:

   ?- Clauses = [[p,not(q)], [not(p),not(s)], [s,not(q)], [q]],
      pl_resolution(Clauses, Rs),
      maplist(writeln, Rs).
   %@ [p,not(q)]-[not(p),not(s)]-->[not(q),not(s)]
   %@ [s,not(q)]-[not(q),not(s)]-->[not(q)]
   %@ [q]-[not(q)]-->[]

   Iterative deepening is used to find a shortest refutation.

- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */


pl_resolution(Clauses0, Chain) :-
        maplist(sort, Clauses0, Clauses), % remove duplicates
        length(Chain, _),
        pl_derive_empty_clause(Chain, Clauses).

pl_derive_empty_clause([], Clauses) :-
        member([], Clauses).
pl_derive_empty_clause([C|Cs], Clauses) :-
        pl_resolvent(C, Clauses, Rs),
        pl_derive_empty_clause(Cs, [Rs|Clauses]).

pl_resolvent((As0-Bs0) --> Rs, Clauses, Rs) :-
        member(As0, Clauses),
        member(Bs0, Clauses),
        select(Q, As0, As),
        select(not(Q), Bs0, Bs),
        append(As, Bs, Rs0),
        sort(Rs0, Rs), % remove duplicates
        maplist(dif(Rs), Clauses).

This may be a lot shorter but (as is often the case with Prolog programs) its operation is fairly opaque to me. In Lisp you see what you're doing; in Prolog you have to imagine execution through a complex, sprawling and invisible search tree.

I prefer Lisp.

---

And here's a resolution prover for the propositional calculus in Python.

Like I said, I prefer Lisp.