Re: leanTap wasn't a good idea

Actually I don't know why prove2/2 is slower than prove/1.
Its not because of A->B, because the urquhart/2 examples
don't contain A->B.
So maybe prefering (A<->B) over - (A<->B) does the job?
Changing this line:
prove2([- (A<->B)|L],R) :- !, prove2([-A,-B|L],R), prove2([B,A|L],R).
Into this line:
prove2([- (A<->B)|L],R) :- !, prove2([-B,-A|L],R), prove2([A,B|L],R).
Also changes the performance:
?- urquhart(12,X), time(prove2([X],[])).
% Zeit 22261 ms, GC 0 ms, Lips 7011361, Uhr 09.12.2024 15:33
Maybe should try something what Jens Otten does in one
of its provers. Some heuristic ordering based on
formula measurement.
Mild Shock schrieb:

Hi,
 Refering to this idea:
 leanTAP revisited - Melvin Fitting
https://www.researchgate.net/publication/2240690
 Some benchmark results:
 /* non-leanTap, prefers A->B over other forms */
?- urquhart(12,X), time(prove([X])).
% Zeit 2104 ms, GC 16 ms, Lips 6894483, Uhr 09.12.2024 15:15
 /* leanTap, works strictly left to right */
?- urquhart(12,X), time(prove2([X],[])).
% Zeit 81174 ms, GC 0 ms, Lips 6679748, Uhr 09.12.2024 15:12
 The source code:
 /* non-leanTap, prefers A->B over other forms */
prove(L) :- select(-A,L,R), member(A,R), !.
prove(L) :- select((A->B),L,R), !, prove([-A,B|R]).
prove(L) :- select((A<->B),L,R), !, prove([-A,B|R]), prove([-B,A|R]).
prove(L) :- select(- (A->B),L,R), !, prove([A|R]), prove([-B|R]).
prove(L) :- select(- (A<->B),L,R), !, prove([-A,-B|R]), prove([B,A|R]).
 /* leanTap, works strictly left to right */
prove2([(A->B)|L],R) :- !, prove2([-A,B|L],R).
prove2([(A<->B)|L],R) :- !, prove2([-A,B|L],R), prove2([-B,A|L],R).
prove2([- (A->B)|L],R) :- !, prove2([A|L],R), prove2([-B|L],R).
prove2([- (A<->B)|L],R) :- !, prove2([-A,-B|L],R), prove2([B,A|L],R).
prove2([A|_],R) :- member(-A,R), !.
prove2([-A|_],R) :- member(A,R), !.
prove2([A|L],R) :- prove2(L,[A|R]).