🚀 go-pugleaf

About a year ago there was some discussion on the net which left the 
impression that Prolog was not as good a language as C for writing 
resolution theorem provers.  This impression was due to the 
benchmark results of two implementations (one in C and one in 
Prolog) of the same "set-of-support strategy" resolution algorithm.  
On a Sun-3, some contradictions took the C version about 1.4 seconds 
to refute whereas the Prolog version took between 30 seconds and 2 
minutes.  Some optimizations were done on the Prolog code by a 
number of people and the discrepancy was reduced by a factor of 5, 
but the resulting code was still about an order of magnitude slower 
than the C version.  For another contradiction, the propositional 
formulas that express the idea that 5 objects can't fit into 4 holes, 
which is known to belong to a class of problems that are hard for 
*every* resolution proving method (Haken 1985), the C version took 
between 10 and 15 minutes on a Sun-3.  The Prolog version took too 
long to be worth measuring.

The moral of the story drawn by the implementors was that since 
the C and Prolog versions of this algorithm performed the same 
computations, something about Prolog, viz. the lack of destructive 
assignment, was probably at fault.

The purpose of the exercise, of course, was not to write the best 
theorem prover in each language but to compare similar operations 
in two languages that have radically different programming models.  
However, I would suggests that another conclusion be drawn: 
different programming paradigms demand different algorithms.  
While this is perhaps obvious to some, I thought that the following 6-
line theorem prover in (pure) Prolog nicely illustrates the point.

For the examples that were used in the benchmark exercise, this 
analytic tableau theorem prover is several orders of magnitude 
faster than even the 'C' version of the set-of- support resolution 
prover.  However, it is not necessarily a better theorem proving 
method.  I know that there are examples which are exponentially  
harder for Analytic Tableau than for Resolution (by which I mean 
that the number of lines in the resolution proof, as opposed to the 
number of computations needed to find it, is vastly shorter than the 
size of the shortest analytic tableau).  So I wouldn't at all be 
surprized if there are some examples that defeat this analytic 
tableau program but are feasibly provable using set-of-support 
resolution.

The idea behind this theorem prover is a variation on the Analytic 
Tableau method (Smullyan 1968).  Since it is the variation on this 
method that makes this program relatively efficient, it deserves 
some explanation.  

A conjunction of disjunctive formulas is satisfiable if each disjunction 
can be satisfied.  We represent each disjunction as a list of literals 
and the conjunction as a list of disjunctions. For each disjunctive 
formula an attempt is made to provide a satisfying assignment to at 
least one propositional variable in that formula.  If we represent 
each propositional variable by a (first-order) logic variable in Prolog, 
this truth-value assignment is propagated to all the occurrences of 
this propositional variable in every formula simply by unification.

A formula is disjunction (list) of literals of the form              
literal(NegOrPos,Variable) where NegOrPos indicates the presence or 
absence of a negation sign in front of the Variable.  For example the 
clause ((a v ~b) & (b v ~c) is represented as         
[[literal(true,A),literal(false,B)],[literal(true,B),literal(false,C)]].   A 
formula is satisfied if a variable can be unified with its prefix (true 
or false). 

The first two lines are easy.  A conjunction (list) of formulas is 
satisfiable if each formula can be satisfied.

satisfiable([]).
satisfiable([F|Formulas]) :- satisfied(F),satisfiable(Formulas).

The naive program to check that a disjunctive formula is satisfied is 
analogous to member/2:

satisfied([literal(T,T)|_]).         % the first disjunct is satisfied
satisfied([_|R]) :- satisfied(R).    % or one of the rest is

(This program, incidentally, is equivalent in complexity to 
L. Pereira's theorem prover in "Prolog by Example" by Coelho and 
Cotta (1988) a version of which is reproduced at the end of this 
article.)

There are two major problems with this program:
(1) it will explore unnecessary truth-value assignments for clauses 
that are already true in virtue of a previous truth-value assignment 
to another literal.
(2) it does not take advantage of the fact that once it has shown that 
a truth-value assignment for a literal in a clause cannot be used to 
satisfy the other clauses then only its negation can.

The beauty of it is that *both* these optimizations are 
implemented immediately by the following modifications:

satisfied([literal(T,T)|_]).
satisfied([literal(TV,V) | Literals]):- negation(TV,V),satisfied(Literals).

negation(true,false).
negation(false,true).

If the attempt to satisfy a disjunctive formula (the first clause for 
satisfied/1) fails then the literal is falsified (the truth-value 
reversed) and another literal in that formula must be satisfied.  Thus, 
if the second clause to satisfied/1 is called with a variable already 
bound to a satisfying assignment, then looking at the others is 
unnecessary, which is guaranteed by the failure of the guard 
negation/2 (optimization 1).  And if satisfied/1 was originally called 
with an unbound variable and backtracking causes the second clause 
for satisfied to be called, then the literal can have its truth-value 
reversed by the call to negation/2 (optimization 2).

Prolog systems with indexing may benefit further by folding 
in negation/2 into the head of satisfy/1, 

satisfied([literal(T,T)|_]).
satisfied([literal(true,false) | Literals]):- satisfied(Literals).
satisfied([literal(false,true) | Literals]):- satisfied(Literals).

making it a 5 line program.

It turns out that, for minimally inconsistent sets of formulas like the 
5 objects in 4 holes problem, this program is a couple of orders of 
magnitude faster (about 10 seconds on a Mac-II using a 5K-lips 
Prolog) than the C program that implements the set-of-support 
resolution prover on a Sun-3.  Of course, they _are_ different 
algorithms and this one is not optimized to handle non-minimally 
inconsistent sets.

What this may illustrate is that while a procedural language like C 
probably lends itself well to deterministic algorithms like set-of-
support resolution, Prolog is better suited to non-deterministic 
semantic techniques.

BIBLIOGRAPHY

Smullyan, R., (1968). _First Order Logic_ Springer-Verlag, New 
York,.Haken, A. (1985).  "The Intractability of Resolution" 
_Theoretical Computer Science_ 39 pp.297-308.

Andre Vellino
Computing Research Laborartory           TEL: (613) 763-7514
Bell-Northern Research                   FAX: (613) 763-4222
P.O. BOX 3511 Station C                  BITNET: vellino@bnr.ca
Ottawa, Ontario                          UUCP: utzoo!bnr-vpa!bnr-di!anv
Canada K1Y 4H7                                 @ ai.utoronto

% --------------------------- cut here ------------
satisfiable( [] ).
satisfiable([F|Formulas]) :- satisfied(F), satisfiable(Formulas).

satisfied([literal(T,T)|_]).
satisfied([literal(TV,V) | Literals]):-negation(TV,V),satisfied(Literals).

negation(true,false).
negation(false,true).

%%%    5 objects can't fit into 4 holes !
formulas( [ 
  [literal(true,_a),literal(true,_b),literal(true,_c),literal(true,_d)],
  [literal(true,_e),literal(true,_f),literal(true,_g),literal(true,_h)],
  [literal(true,_i),literal(true,_j),literal(true,_k),literal(true,_l)],
  [literal(true,_m),literal(true,_n),literal(true,_o),literal(true,_p)],
  [literal(true,_q),literal(true,_r),literal(true,_s),literal(true,_t)],
  [literal(false, _a), literal(false, _e)],
  [literal(false, _a), literal(false, _i)],
  [literal(false, _a), literal(false, _m)],
  [literal(false, _a), literal(false, _q)],
  [literal(false, _b), literal(false, _f)],
  [literal(false, _b), literal(false, _j)],
  [literal(false, _b), literal(false, _n)],
  [literal(false, _b), literal(false, _r)],
  [literal(false, _c), literal(false, _g)],
  [literal(false, _c), literal(false, _k)],
  [literal(false, _c), literal(false, _o)],
  [literal(false, _c), literal(false, _s)],
  [literal(false, _d), literal(false, _h)],
  [literal(false, _d), literal(false, _l)],
  [literal(false, _d), literal(false, _p)],
  [literal(false, _d), literal(false, _t)],
  [literal(false, _e), literal(false, _i)],
  [literal(false, _e), literal(false, _m)],
  [literal(false, _e), literal(false, _q)],
  [literal(false, _f), literal(false, _j)],
  [literal(false, _f), literal(false, _n)],
  [literal(false, _f), literal(false, _r)],
  [literal(false, _g), literal(false, _k)],
  [literal(false, _g), literal(false, _o)],
  [literal(false, _g), literal(false, _s)],
  [literal(false, _h), literal(false, _l)],
  [literal(false, _h), literal(false, _p)],
  [literal(false, _h), literal(false, _t)],
  [literal(false, _i), literal(false, _m)],
  [literal(false, _i), literal(false, _q)],
  [literal(false, _j), literal(false, _n)],
  [literal(false, _j), literal(false, _r)],
  [literal(false, _k), literal(false, _o)],
  [literal(false, _k), literal(false, _s)],
  [literal(false, _l), literal(false, _p)],
  [literal(false, _l), literal(false, _t)],
  [literal(false, _m), literal(false, _q)],
  [literal(false, _n), literal(false, _r)],
  [literal(false, _o), literal(false, _s)],
  [literal(false, _p), literal(false, _t)]   ] ). 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Truth-table technique used in L. Pereira's program (1976)

sat((A & B)) :-    sat(A), sat(B).
sat((A ; B)) :-    sat(A) ; sat(B).

sat(pos(true)).
sat(neg(false)).