Thanks for this point. I nevertheless delete my previous version of quine-wang.pl because working on the order of rules, I get a very best result. I give in the file the new result. Here is the new quine-wang.pl:
% A Propositional Theorem Prover using Wang's Algorithm
% that makes use of Boole's method (Jan Burse work) for counter-models search.
% :- use_module(library(ordsets)).
% :- use_module(library(statistics)).
% :- use_module(library(dcg/basics)).
% :- use_module(library(clpfd)).
:- op( 500, fy, ~). % negation
:- op(1000, xfy, &). % conjunction
:- op(1100, xfy, v). % disjunction
:- op(1110, xfy, =>). % conditional
:- op(1120, xfy, <=>). % biconditional
:- op(1200,xfy, -->). % implication (sequent)
%TYPE 'qw.' INTO THE CONSOLE TO START
help:-
write('-----------------------------------------------------------'),nl,
write('\nA Propositional Theorem Prover using both Quine\'s and Wang\'s Algorithms\n'),
write('by Joseph Vidal-Rosset from Ben Hudson\'s and Isabelle-Newbie\'s programs.\n\n'),
write('https://github.com/benhuds?tab=repositories \n\n'),
write('https://stackoverflow.com/questions/63505466/prolog-implementation-of-quines-algorithm-for-classical-propositional-logic-in\n\n'),
write('-----------------------------------------------------------'),nl,
write('To test the validity of your formula with Wang\'s algorithm:\n'),
write('- First, write "qw." and press Enter.\n'),
write('- Second, with this usual syntax: ~ a | a & b | a v b | a => b| a <=> b| \n'),
write('write your propositional formula and press Enter.\n'),
write('That\'s it. Have fun!').
qw :-
read(Formula),
getFormula(Formula).
getFormula(Formula):-
nl,
write('Quine:'),
time((nl,\+quine(Formula))),
write('to prove that this formula is invalid.'),nl,
qw
;
write('to prove that this formula is valid.'),nl,nl,
go([] --> [Formula]).
go(Formula):-
write('Wang:'),
nl,
write(' \t'),write(Formula),
time(prove(Formula)),
write('to prove that '),write(Formula), write(' is a theorem in Classical Propositional Logic.\n'),
qw.
%predicate to delete an element X from a list L.
del(X,[X|Tail],Tail).
del(X,[H|Tl1],[H|Tl2]):-
del(X,Tl1,Tl2),!.
%rule for id* (Ax.)
prove(L --> R):-
member(A,L),
member(B,R),
A == B,
nl,write(' \tDone (by id*)'),nl,nl.
%non-branching rules
prove(L --> R):-
member(A & B,L),
del(A & B,L,NewL),!,
nl,write(' \t'),write([A,B|NewL] --> R),
write(' \t (by and/left)'),
prove([A,B|NewL] --> R).
prove(L --> R):-
member(A v B,R),
del(A v B,R,NewR),!,
nl,write(' \t'),write(L --> [A,B|NewR]),
write(' \t (by or/right)'),
prove(L --> [A,B|NewR]).
prove(L --> R):-
member(A => B,R),!,
del(A => B,R,NewR),
nl,write(' \t'),write([A|L] --> [B|NewR]),
write(' \t (by arrow/right)'),
prove([A|L] --> [B|NewR]).
%branching rules
prove(L --> R):-
member(A => B,L),
del(A => B,L,NewL),!,
nl,write(' \tFirst branch: '),
nl,write(' \t'),write([B|NewL] --> R),
write(' \t (by arrow/left)'),
prove([B|NewL] --> R),
nl,write(' \tSecond branch: '),
nl,write(' \t'),write(NewL --> [A|R]),
write(' \t (by arrow/left)'),
prove(NewL --> [A|R]).
prove(L --> R):-
member(A & B,R),
del(A & B,R,NewR),!,
nl,write(' \tFirst branch: '),
nl,write(' \t'),write(L --> [A|NewR]),
write(' \t (by and/right)'),
prove(L --> [A|NewR]),
nl,write(' \tSecond branch: '),
nl,write(' \t'),write(L --> [B|NewR]),
write(' \t (by and/right)'),
prove(L --> [B|NewR]).
prove(L --> R):-
member(A v B,L),
del(A v B,L,NewL),!,
nl,write(' \tFirst branch: '),
nl,write(' \t'),write([A|NewL] --> R),
write(' \t (by or/left)'),
prove([A|NewL] --> R),
nl,write(' \tSecond branch: '),
nl,write(' \t'),write([B|NewL] --> R),
write(' \t (by or/left)'),
prove([B|NewL] --> R).
%negation
prove(L --> R):-
member(~X,L),
del(~X,L,NewL),!,
nl,write(' \t'),write(NewL --> [X|R]),
write(' \t (by negation/left)'),
prove(NewL --> [X|R]).
prove(L --> R):-
member(~X,R),
del(~X,R,NewR),!,
nl,write(' \t'),write([X|L] --> NewR),
write(' \t (by negation/right)'),
prove([X|L] --> NewR).
%rules for biconditional
prove(L --> R):-
member(A <=> B,L),
del(A <=> B,L,NewL),!,
nl,write(' \t'),write([(A => B),(B => A)|NewL] --> R),
write(' \t (by and/left)'),
prove([(A => B),(B => A)|NewL] --> R).
prove(L --> R):-
member(A <=> B,R),
del(A <=> B,R,NewR),!,
nl,write(' \t'),write(L --> [(A => B) & (B => A)|NewR]),
write(' \t (by and/right)'),
prove(L --> [(A => B) & (B => A)|NewR]).
% Quine
formula_simpler(~ ~ P , P).
formula_simpler(~ ⊥, ⊤).
formula_simpler(~ ⊤, ⊥).
formula_simpler(_P & ⊥, ⊥).
formula_simpler(⊥ & _P, ⊥).
formula_simpler(P & ⊤, P).
formula_simpler(⊤ & P, P).
formula_simpler(P v ⊥, P).
formula_simpler(⊥ v P, P).
formula_simpler(_P v ⊤, ⊤).
formula_simpler(⊤ v _P, ⊤).
formula_simpler(P => ⊥, ~ P).
formula_simpler(_P => ⊤, ⊤).
formula_simpler(⊥ => _P, ⊤).
formula_simpler(⊤ => P, P).
formula_simpler(P <=> ⊥, ~ P).
formula_simpler(⊥ <=> P, ~ P).
formula_simpler(P <=> ⊤, P).
formula_simpler(⊤ <=> P, P).
formula_simpler(P <=> P, ⊤).
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 ).
formula_variable(Variable, Variable) :-
atom(Variable),
dif(Variable, ⊤),!,
atom(Variable),
dif(Variable, ⊥).
formula_variable(Formula, Variable) :-
Formula =.. [_Operator | Args],
member(Arg, Args),
formula_variable(Arg, Variable),!.
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].
quine(Formula) :-
formula_simple2(Formula, ⊤),
write(⊤),!.
quine(Formula) :-
formula_simple2(Formula, SimpleFormula),
formula_variable(SimpleFormula, Variable),
!,
variable_replacement_formula_replaced(Variable, ⊤, Formula, TopFormula),nl,
write(' \t'),write('T is substituted for '),write(Variable),nl,
write(' \t'),write(TopFormula),nl,
write(' \t'),quine(TopFormula),nl,
variable_replacement_formula_replaced(Variable, ⊥, Formula, BotFormula),nl,
write(' \t'),write('⊥ is substituted for '),write(Variable),nl,
write(' \t'),write(BotFormula),nl,
write(' \t'),quine(BotFormula).
/*
Examples:
?- qw.
|: p.
Quine:
T is substituted for p
⊤
⊤
⊥ is substituted for p
⊥
% 35,822 inferences, 0.006 CPU in 0.006 seconds (100% CPU, 6215434 Lips)
to prove that this formula is invalid.
|: (~ p => p) <=> p.
Quine:
T is substituted for p
~ ⊤ => ⊤ <=> ⊤
⊤
⊥ is substituted for p
~ ⊥ => ⊥ <=> ⊥
⊤
% 25,057 inferences, 0.007 CPU in 0.007 seconds (100% CPU, 3777683 Lips)
to prove that this formula is valid.
Wang:
[]-->[(~p=>p<=>p)]
[]-->[(((~p=>p)=>p)&(p=> ~p=>p))] (by and/right)
First branch:
[]-->[((~p=>p)=>p)] (by and/right)
[(~p=>p)]-->[p] (by arrow/right)
First branch:
[p]-->[p] (by arrow/left)
Done (by id*)
Second branch:
[]-->[~p,p] (by arrow/left)
[p]-->[p] (by negation/right)
Done (by id*)
Second branch:
[]-->[(p=> ~p=>p)] (by and/right)
[p]-->[(~p=>p)] (by arrow/right)
[~p,p]-->[p] (by arrow/right)
Done (by id*)
% 172 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 1979150 Lips)
to prove that []-->[(~p=>p<=>p)] is a theorem in Classical Propositional Logic.
|: ((a => b) => a) => a.
Quine:
T is substituted for a
((⊤ => b)=> ⊤)=> ⊤
⊤
⊥ is substituted for a
((⊥ => b)=> ⊥)=> ⊥
⊤
% 426 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 1233306 Lips)
to prove that this formula is valid.
Wang:
[]-->[(((a=>b)=>a)=>a)]
[((a=>b)=>a)]-->[a] (by arrow/right)
First branch:
[a]-->[a] (by arrow/left)
Done (by id*)
Second branch:
[]-->[(a=>b),a] (by arrow/left)
[a]-->[b,a] (by arrow/right)
Done (by id*)
% 78 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 420648 Lips)
to prove that []-->[(((a=>b)=>a)=>a)] is a theorem in Classical Propositional Logic.
|:
Performances:
1. The valid formula:
(((( a0 => f) & ((( b20 => b0) => a20) & ((( b0 => a1) => a0) & (
(( b1 => a2) => a1) & ((( b2 => a3) => a2) & ((( b3 => a4) => a3) &
((( b4 => a5) => a4) & ((( b5 => a6) => a5) & ((( b6 => a7) => a6)
& ((( b7 => a8) => a7) & ((( b8 => a9) => a8) & ((( b9 => a10) =>
a9) & ((( b10 => a11) => a10) & ( (( b11 => a12) => a11) & ((( b12
=> a13) => a12) & ((( b13 => a14) => a13) & ((( b14 => a15) => a14)
& ((( b15 => a16) => a15) & ((( b16 => a17) => a16) & ((( b17 =>
a18) => a17) & ((( b18 => a19) => a18) & ((b19 => a20) => a19))))
)))))))))))))))))) => f) & (((( b19 => a20) => a19)
& ((( b18 => a19) => a18) & ((( b17 => a18) => a17) & ((( b16 =>
a17) => a16) & ((( b15 => a16) => a15) & ((( b14 => a15) => a14) & (
(( b13 => a14) => a13) & ((( b12 => a13) => a12) & ((( b11 => a12)
=> a11) & ((( b10 => a11) => a10) & ((( b9 => a10) => a9) & ((( b8
=> a9) => a8) & ((( b7 => a8) => a7) & ((( b6 => a7) => a6) & (((
b5 => a6) => a5) & ((( b4 => a5) => a4) & ((( b3 => a4) => a3) & ((
( b2 => a3) => a2) & ((( b1 => a2) => a1) & ((( b0 => a1) => a0) & (
(( b20 => b0) => a20) & ( a0 => f)))))))))))))))))))))) => f))
is proved by quine-wang.pl :
Quine:
% 1,013,782 inferences, 0.168 CPU in 0.922 seconds (18% CPU, 6023924 Lips)
to prove that this formula is valid.
Wang:
% 183,434 inferences, 0.046 CPU in 0.768 seconds (6% CPU, 3966894 Lips)
to prove that []-->[(((a0=>f)&((b20=>b0)=>a20)&((b0=>a1)=>a0)&((b1=>a2)=>a1)&((b2=>a3)=>a2)&((b3=>a4)=>a3)&((b4=>a5)=>a4)&((b5=>a6)=>a5)&((b6=>a7)=>a6)&((b7=>a8)=>a7)&((b8=>a9)=>a8)&((b9=>a10)=>a9)&((b10=>a11)=>a10)&((b11=>a12)=>a11)&((b12=>a13)=>a12)&((b13=>a14)=>a13)&((b14=>a15)=>a14)&((b15=>a16)=>a15)&((b16=>a17)=>a16)&((b17=>a18)=>a17)&((b18=>a19)=>a18)&((b19=>a20)=>a19)=>f)&(((b19=>a20)=>a19)&((b18=>a19)=>a18)&((b17=>a18)=>a17)&((b16=>a17)=>a16)&((b15=>a16)=>a15)&((b14=>a15)=>a14)&((b13=>a14)=>a13)&((b12=>a13)=>a12)&((b11=>a12)=>a11)&((b10=>a11)=>a10)&((b9=>a10)=>a9)&((b8=>a9)=>a8)&((b7=>a8)=>a7)&((b6=>a7)=>a6)&((b5=>a6)=>a5)&((b4=>a5)=>a4)&((b3=>a4)=>a3)&((b2=>a3)=>a2)&((b1=>a2)=>a1)&((b0=>a1)=>a0)&((b20=>b0)=>a20)&(a0=>f)=>f))] is a theorem in Classical Propositional Logic.
with working on the order of rules and adding cut after del/1, as suggested by Jan Burse https://swi-prolog.discourse.group/t/improving-wangs-algorithm-in-prolog/2872/115 :
% 160,203 inferences, 0.034 CPU in 0.284 seconds (12% CPU, 4700335 Lips)
to prove that []-->[(((a0=>f)&((b20=>b0)=>a20)&((b0=>a1)=>a0)&((b1=>a2)=>a1)&((b2=>a3)=>a2)&((b3=>a4)=>a3)&((b4=>a5)=>a4)&((b5=>a6)=>a5)&((b6=>a7)=>a6)&((b7=>a8)=>a7)&((b8=>a9)=>a8)&((b9=>a10)=>a9)&((b10=>a11)=>a10)&((b11=>a12)=>a11)&((b12=>a13)=>a12)&((b13=>a14)=>a13)&((b14=>a15)=>a14)&((b15=>a16)=>a15)&((b16=>a17)=>a16)&((b17=>a18)=>a17)&((b18=>a19)=>a18)&((b19=>a20)=>a19)=>f)&(((b19=>a20)=>a19)&((b18=>a19)=>a18)&((b17=>a18)=>a17)&((b16=>a17)=>a16)&((b15=>a16)=>a15)&((b14=>a15)=>a14)&((b13=>a14)=>a13)&((b12=>a13)=>a12)&((b11=>a12)=>a11)&((b10=>a11)=>a10)&((b9=>a10)=>a9)&((b8=>a9)=>a8)&((b7=>a8)=>a7)&((b6=>a7)=>a6)&((b5=>a6)=>a5)&((b4=>a5)=>a4)&((b3=>a4)=>a3)&((b2=>a3)=>a2)&((b1=>a2)=>a1)&((b0=>a1)=>a0)&((b20=>b0)=>a20)&(a0=>f)=>f))] is a theorem in Classical Propositional Logic.
2. The invalid disjunctive formula :
(( o11 & o21 ) v ( ( o11 & o31 ) v ( ( o11 & o41 ) v ( ( o11 & o51 ) v ( ( o11 & o61 ) v ( ( o21 & o31 ) v ( ( o21 & o41 ) v ( ( o21 & o51 ) v ( ( o21 & o61 ) v ( ( o31 & o41 ) v ( ( o31 & o51 ) v ( ( o31 & o61 ) v ( ( o41 & o51 ) v ( ( o41 & o61 ) v ( ( o51 & o61 ) v ( ( o12 & o22 ) v ( ( o12 & o32 ) v ( ( o12 & o42 ) v ( ( o12 & o52 ) v ( ( o12 & o62 ) v ( ( o22 & o32 ) v ( ( o22 & o42 ) v ( ( o22 & o52 ) v ( ( o22 & o62 ) v ( ( o32 & o42 ) v ( ( o32 & o52 ) v ( ( o32 & o62 ) v ( ( o42 & o52 ) v ( ( o42 & o62 ) v ( ( o52 & o62 ) v ( ( o13 & o23 ) v ( ( o13 & o33 ) v ( ( o13 & o43 ) v ( ( o13 & o53 ) v ( ( o13 & o63 ) v ( ( o23 & o33 ) v ( ( o23 & o43 ) v ( ( o23 & o53 ) v ( ( o23 & o63 ) v ( ( o33 & o43 ) v ( ( o33 & o53 ) v ( ( o33 & o63 ) v ( ( o43 & o53 ) v ( ( o43 & o63 ) v ( ( o53 & o63 ) v ( ( o14 & o24 ) v ( ( o14 & o34 ) v ( ( o14 & o44 ) v ( ( o14 & o54 ) v ( ( o14 & o64 ) v ( ( o24 & o34 ) v ( ( o24 & o44 ) v ( ( o24 & o54 ) v ( ( o24 & o64 ) v ( ( o34 & o44 ) v ( ( o34 & o54 ) v ( ( o34 & o64 ) v ( ( o44 & o54 ) v ( ( o44 & o64 ) v ( ( o54 & o64 ) v ( ( o15 & o25 ) v ( ( o15 & o35 ) v ( ( o15 & o45 ) v ( ( o15 & o55 ) v ( ( o15 & o65 ) v ( ( o25 & o35 ) v ( ( o25 & o45 ) v ( ( o25 & o55 ) v ( ( o25 & o65 ) v ( ( o35 & o45 ) v ( ( o35 & o55 ) v ( ( o35 & o65 ) v ( ( o45 & o55 ) v ( ( o45 & o65 ) v ( o55 & o65 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
is proved as being such via Quine:
% 403,094 inferences, 0.051 CPU in 0.230 seconds (22% CPU, 7922030 Lips)
to prove that this formula is invalid.
*/