Prolog implementation of Quine's algorithm for classical propositional logic (in Quine's "Methods of Logic")

Question

I know only one prover that translates the algorithm that Quine gave for classical propositional logic in his book Methods of Logic (Harvard University Press, 1982, ch. 1 sec. 5, pp. 33-40), this prover is in Haskell and it is here: Quine's algorithm in Haskell

I tried to translate Quine's algorithm in Prolog, but until now I have not succeeded. It is a pity because it is an efficient algorithm and a Prolog translation would be interesting. I am going to describe this algorithm. The only Prolog code that I give at the start is the list of operators that would be useful to test the prover:

% operator definitions (TPTP syntax)

:- op( 500, fy, ~).      % negation
:- op(1000, xfy, &).     % conjunction
:- op(1100, xfy, '|').   % disjunction
:- op(1110, xfy, =>).    % conditional
:- op(1120, xfy, <=>).   % biconditional

Truth constants are top and bot for, respectively, true and false. The algorithm starts as follows: For any propositional formula F, make two copies of it and replace the atom which has the highest occurrence in F by top in the first copy, and by bot in the second copy, and then apply the following ten reduction rules one rule at a time for as many times as possible, for each of the copies:

 1.  p & bot  --> bot
 2.  p & top  --> p
 3.  p | bot  --> p
 4.  p | top  --> top
 5.  p => bot --> ~p 
 6.  p => top --> top
 7.  bot => p --> top
 8.  top => p -->  p
 9.  p <=> bot --> ~p
 10. p <=> top --> p

Of course, we have also the following rules for negation and double negation:

 1. ~bot --> top
 2. ~top --> bot
 3. ~~p  --> p 

When there is neither top nor bot in the formula so none of the rules apply, split it again and pick one atom to replace it by top and by bot in yet another two sided table. The formula F is proved if and only if the algorithm ends with top in all copies, and fails to be proved, otherwise.

Example:

                         (p => q) <=> (~q => ~p)

 (p => top) <=> (bot => ~p)                 (p => bot) <=> (top => ~p)

       top  <=>  top                              ~p   <=>  ~p  

            top                       top <=> top                bot <=> bot

                                          top                        top

It is clear that Quine's algorithm is an optimization of the truth tables method, but starting from codes of program of truth tables generator, I did not succeed to get it in Prolog code.

A help at least to start would be welcome. In advance, many thanks.

---

EDIT by Guy Coder

This is double posted at SWI-Prolog forum which has a lively discussion and where provers Prolog are published but not reproduced in this page.

Answer 1

Here is a skeleton of solution. I hope it can help you fill the holes.

is_valid(Formula) :-
    \+ derive(Formula,bot).

is_satisfiable(Formula) :-
    derive(Formula, top).

derive(bot,D):-
    !,
    D=bot.
derive(top,D):-
    !,
    D=top.
derive(Formula,D):-
    reduce(Formula, Formula1),
    (
      Formula=Formula1
    ->
      branch(Formula1,D)
    ;
      derive(Formula1,D)
    ).

Now you need to implement reduce/2 that applies the reduction rules (recursively in the sub-formulas), and branch/2 that replaces non-deterministically an atom of the formula with either top or bot, then calls recursively derive/2. Something like:

branch(Formula, D):-
    pickAtom(Formula, Atom),
    (
      Rep=top
    ; 
      Rep=bot
    ),
    replace(Formula, Atom, Rep, Formula1),
    derive(Formula1,D).

Answer 2

Warning! We dont use TPTP syntax, but syntax from SWI-Prolog CLP(B). Seems that this brute force method is older (*), and as Prolog code its so small, it even fits into the pocket of your trousers:

Here is a full implementation. The cut is only used to priorize the rewriting and corresponds pretty much Haskell rules. Except that Haskell might not have a datatype logical variable like Prolog:

:- op(300, fy, ~).

eval(A, A) :- var(A), !.
eval(A+B, R) :- !, eval(A, X), eval(B, Y), simp(X+Y, R).
eval(A*B, R) :- !, eval(A, X), eval(B, Y), simp(X*Y, R).
eval(~A, R) :- !, eval(A, X), simp(~X, R).
eval(A, A).

simp(A, A) :- var(A), !.
simp(A+B, B) :- A == 0, !.
simp(A+B, A) :- B == 0, !.
simp(A+_, 1) :- A == 1, !.
simp(_+B, 1) :- B == 1, !.
simp(A*_, 0) :- A == 0, !.
simp(_*B, 0) :- B == 0, !.
simp(A*B, B) :- A == 1, !.
simp(A*B, A) :- B == 1, !.
simp(~A, 1) :- A == 0, !.
simp(~A, 0) :- A == 1, !.
simp(A, A).

The code is not pure Prolog and uses non-logical var/1, (==)/2, etc.. meta programming. Like Boole we linearly reduce and perform a conjunction of the two substitutions, so we do the Quine split without some branching and via a single front:

judge(A, [B|R]) :- eval(A, B), 
                   term_variables(B, L), judge(B, L, R).

judge(_, [], R) :- !, R = [].
judge(A, [B|L], R) :-
  copy_term(A-[B|L], C-[0|L]),
  copy_term(A-[B|L], D-[1|L]), judge(C*D, R).

In the above we use copy_term/2 to do substitution. The idea is borrowed from Ulrich Neumerkels lambda library. We need to also make available =< and =:= in eval/2 and simp/2. For full source code see here. Here are example runs in any of your favorite ISO Prolog:

?- judge(A+ ~A, L).
L = [A+ ~A, 1] /* Ends in 1, Tautology */

?- judge(A+ ~B, L).
L = [A+ ~B, ~B, 0] /* Ends in 0, Falsifiable */

?- judge(((P+Q)=<R)=:=((P=<R)*(Q=<R)), L).
L = [(P+Q =< R) =:= (P =< R)*(Q =< R),
  ((Q =< R) =:= (Q =< R))*(R =:= R*(Q =< R)),
  (R =:= R)*((R =:= R)*(R =:= R*R)), 1].  

(*) From:
U. Martin and T. Nipkow. Boolean unification—the story so far.
In Unification, pages 437–455. Academic Press, London, 1990.

Answer 3

The Haskell code seemed complicated to me. Here's an implementation based on the description of the algorithm given in the question. (Using maplist and dif from the SWI-Prolog library, but easy to make self-contained.)

First, single simplification steps:

formula_simpler(_P & bot,   bot).
formula_simpler(P & top,    P).
formula_simpler(P '|' bot,  P).
formula_simpler(_P '|' top, top).  % not P as in the question
formula_simpler(P => bot,   ~P).
formula_simpler(_P => top,  top).
formula_simpler(bot => _P,  top).
formula_simpler(top => P,   P).
formula_simpler(P <=> bot,  ~P).
formula_simpler(P <=> top,  P).
formula_simpler(~bot,       top).
formula_simpler(~top,       bot).
formula_simpler(~(~P),      P).

Then, iterated application of these steps to subterms and iteration at the root until nothing changes anymore:

formula_simple(Formula, Simple) :-
    Formula =.. [Operator | Args],
    maplist(formula_simple, Args, SimpleArgs),
    SimplerFormula =.. [Operator | SimpleArgs],
    (   formula_simpler(SimplerFormula, EvenSimplerFormula)
    ->  formula_simple(EvenSimplerFormula, Simple)
    ;   Simple = SimplerFormula ).

For example:

?- formula_simple(~ ~ ~ ~ ~ a, Simple).
Simple = ~a.

For the replacement of variables by other values, first a predicate for finding variables in formulas:

formula_variable(Variable, Variable) :-
    atom(Variable),
    dif(Variable, top),
    dif(Variable, bot).
formula_variable(Formula, Variable) :-
    Formula =.. [_Operator | Args],
    member(Arg, Args),
    formula_variable(Arg, Variable).

On backtracking this will enumerate all occurrences of variables in a formula, for example:

?- formula_variable((p => q) <=> (~q => ~p), Var).
Var = p ;
Var = q ;
Var = q ;
Var = p ;
false.

This is the only source of nondeterminism in the proof procedure below, and you can insert a cut after the formula_variable call to commit to a single choice.

Now the actual replacement of a Variable in a Formula by Replacement:

variable_replacement_formula_replaced(Variable, Replacement, Variable, Replacement).
variable_replacement_formula_replaced(Variable, _Replacement, Formula, Formula) :-
    atom(Formula),
    dif(Formula, Variable).
variable_replacement_formula_replaced(Variable, Replacement, Formula, Replaced) :-
    Formula =.. [Operator | Args],
    Args = [_ | _],
    maplist(variable_replacement_formula_replaced(Variable, Replacement), Args, ReplacedArgs),
    Replaced =.. [Operator | ReplacedArgs].

And finally the prover, constructing a proof term like the Haskell version:

formula_proof(Formula, trivial(Formula)) :-
    formula_simple(Formula, top).
formula_proof(Formula, split(Formula, Variable, TopProof, BotProof)) :-
    formula_simple(Formula, SimpleFormula),
    formula_variable(SimpleFormula, Variable),
    variable_replacement_formula_replaced(Variable, top, Formula, TopFormula),
    variable_replacement_formula_replaced(Variable, bot, Formula, BotFormula),
    formula_proof(TopFormula, TopProof),
    formula_proof(BotFormula, BotProof).

A proof of the example from the question:

?- formula_proof((p => q) <=> (~q => ~p), Proof).
Proof = split((p=>q<=> ~q=> ~p),
              p,
              split((top=>q<=> ~q=> ~top),
                    q,
                    trivial((top=>top<=> ~top=> ~top)),
                    trivial((top=>bot<=> ~bot=> ~top))),
              trivial((bot=>q<=> ~q=> ~bot))) .

All of its proofs:

?- formula_proof((p => q) <=> (~q => ~p), Proof).
Proof = split((p=>q<=> ~q=> ~p), p, split((top=>q<=> ~q=> ~top), q, trivial((top=>top<=> ~top=> ~top)), trivial((top=>bot<=> ~bot=> ~top))), trivial((bot=>q<=> ~q=> ~bot))) ;
Proof = split((p=>q<=> ~q=> ~p), p, split((top=>q<=> ~q=> ~top), q, trivial((top=>top<=> ~top=> ~top)), trivial((top=>bot<=> ~bot=> ~top))), trivial((bot=>q<=> ~q=> ~bot))) ;
Proof = split((p=>q<=> ~q=> ~p), q, trivial((p=>top<=> ~top=> ~p)), split((p=>bot<=> ~bot=> ~p), p, trivial((top=>bot<=> ~bot=> ~top)), trivial((bot=>bot<=> ~bot=> ~bot)))) ;
Proof = split((p=>q<=> ~q=> ~p), q, trivial((p=>top<=> ~top=> ~p)), split((p=>bot<=> ~bot=> ~p), p, trivial((top=>bot<=> ~bot=> ~top)), trivial((bot=>bot<=> ~bot=> ~bot)))) ;
Proof = split((p=>q<=> ~q=> ~p), q, trivial((p=>top<=> ~top=> ~p)), split((p=>bot<=> ~bot=> ~p), p, trivial((top=>bot<=> ~bot=> ~top)), trivial((bot=>bot<=> ~bot=> ~bot)))) ;
Proof = split((p=>q<=> ~q=> ~p), q, trivial((p=>top<=> ~top=> ~p)), split((p=>bot<=> ~bot=> ~p), p, trivial((top=>bot<=> ~bot=> ~top)), trivial((bot=>bot<=> ~bot=> ~bot)))) ;
Proof = split((p=>q<=> ~q=> ~p), p, split((top=>q<=> ~q=> ~top), q, trivial((top=>top<=> ~top=> ~top)), trivial((top=>bot<=> ~bot=> ~top))), trivial((bot=>q<=> ~q=> ~bot))) ;
Proof = split((p=>q<=> ~q=> ~p), p, split((top=>q<=> ~q=> ~top), q, trivial((top=>top<=> ~top=> ~top)), trivial((top=>bot<=> ~bot=> ~top))), trivial((bot=>q<=> ~q=> ~bot))) ;
false.

This contains lots of redundancy. Again, this is because formula_variable enumerates occurrences of variables. It can be made more deterministic in various ways depending on one's requirements.

EDIT: The above implementation of formula_simple is naive and inefficient: Every time it makes a successful simplification at the root of the formula, it revisits all of the subformulas as well. But on this problem, no new simplifications of the subformulas will become possible when the root is simplified. Here is a new version that is more careful to first fully rewrite the subformulas, and then only iterate rewrites at the root:

formula_simple2(Formula, Simple) :-
    Formula =.. [Operator | Args],
    maplist(formula_simple2, Args, SimpleArgs),
    SimplerFormula =.. [Operator | SimpleArgs],
    formula_rootsimple(SimplerFormula, Simple).

formula_rootsimple(Formula, Simple) :-
    (   formula_simpler(Formula, Simpler)
    ->  formula_rootsimple(Simpler, Simple)
    ;   Simple = Formula ).

This is considerably faster:

?- time(formula_simple(~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~(a & b & c & d & e & f & g & h & i & j & k & l & m & n & o & p & q & r & s & t & u & v & w & x & y & z), Simple)).
% 11,388 inferences, 0.004 CPU in 0.004 seconds (100% CPU, 2676814 Lips)
Simple = ~ (a&b&c&d&e&f&g&h& ... & ...).

?- time(formula_simple2(~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~ ~(a & b & c & d & e & f & g & h & i & j & k & l & m & n & o & p & q & r & s & t & u & v & w & x & y & z), Simple)).
% 988 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 2274642 Lips)
Simple = ~ (a&b&c&d&e&f&g&h& ... & ...).

Edit: As pointed out in the comments, the prover as written above can be veeery slow on slightly bigger formulas. The problem is that I forgot that some operators are commutative! Thanks jnmonette for pointing this out. The rewrite rules must be expanded a bit:

formula_simpler(_P & bot,   bot).
formula_simpler(bot & _P,   bot).
formula_simpler(P & top,    P).
formula_simpler(top & P,    P).
formula_simpler(P '|' bot,  P).
formula_simpler(bot '|' P,  P).
...

And with this the prover behaves nicely.