Exctraction of the Proof from Fitting's leanTap Prolog Prover-CodePudding

Here is the SWI-Prolog code of Fitting's leanTap revisited:

:- use_module(library(lists)).
:- use_module(library(statistics)).

% :- use_module(library(dom)).
% operator definitions (TPTP syntax)

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

/*
Next, a classification of formula types,
& instances.
*/

type(X & Y, conj, X, Y).
type(~(X & Y), disj, ~ X, ~ Y).
type(X | Y, disj, X, Y).
type(~(X | Y), conj, ~ X, ~ Y).
type(X => Y, disj, ~ X, Y).
type(~(X => Y), conj, X, ~ Y).
type(X <=> Y, disj, X & Y, ~ X & ~ Y).
type(~(X <=> Y), disj, X & ~ Y, ~ X & Y).
type(~ (~ (X)), doub, X, _).
/*
Now the heart of the matter.
thm(Lambda, Gamma) :-
the sequent Lambda --> Gamma is provable.
*/

thm(Lambda, [Doubleneg | Gamma]) :- 
        type(Doubleneg, doub, X, _), !,
        thm(Lambda, [X | Gamma]).

thm(Lambda, [Beta | Gamma]) :-
        type(Beta, disj, Beta1, Beta2), !,
        thm(Lambda, [Beta1, Beta2 | Gamma]).

thm(Lambda, [Alpha | Gamma]) :-
        type(Alpha, conj, Alpha1, Alpha2), !,
        thm(Lambda, [Alpha1 | Gamma]), !,
        thm(Lambda, [Alpha2 | Gamma]).

thm([L1|Lambda], [L2|_]) :-
        (
          L1 = L2, !
        ;
          thm(Lambda, [L2])
        ).

thm(Lambda, [~ L | Gamma]) :-
        thm([L | Lambda], Gamma), !.

thm(Lambda, [L | Gamma]) :-
        thm([~ L | Lambda], Gamma), !.
/*
Finally, the driver.
*/
prove(X) :-
time(thm([], [X])).

This code according to Fitting provides a sequent calculus. I have tried to change minimally this code to get a Prolog Print of each proof, with input prove(X, Proof), following the structure of Jen Otten's prover (online here and here):

% -----------------------------------------------------------------
% leanseq.pl - A sequent calculus prover implemented in Prolog
% -----------------------------------------------------------------
:- use_module(library(lists)).

% operator definitions (TPTP syntax)

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

% -----------------------------------------------------------------
provable(F, P) :- time(prove([] > [F], P)).
% -----------------------------------------------------------------

% axiom
prove(G > D, ax(G > D, A)) :- member(A,G), member(B,D), A == B, !.

% conjunction
prove(G > D, land(G > D, P) ) :- select1( (A & B) ,G,G1), !,
                prove([A , B | G1] > D, P).

prove(G > D, rand(G > D, P1,P2)) :- select1( (A & B) ,D,D1), !,
                prove(G > [A|D1], P1), prove(G > [B|D1], P2).

% disjunction
prove(G > D, lor(G > D, P1,P2)) :- select1((A | B),G,G1), !,
                prove([A|G1] > D, P1), prove([B|G1] > D, P2).

prove(G > D, ror(G > D, P)) :- select1( (A | B),D,D1), !,
                prove(G > [A,B|D1], P ).

% implication
prove(G > D, limpl(G > D, P1,P2)) :- select1((A => B),G,G1), !,
                prove(G1 > [A|D], P1), prove([B|G1] > D, P2).

prove(G > D, rimpl(G > D, P)) :- select1((A => B),D,D1), !,
                prove([A|G] > [B|D1], P).

% negation
prove(G > D, lneg(G > D, P)) :- select1( ~A,G,G1), !,
                prove(G1 > [A|D], P).

prove(G > D, rneg(G > D, P)) :- select1(~A ,D,D1), !,
                prove([A|G] > D1, P).

% -----------------------------------------------------------------
select1(X,L,L1) :- append(L2,[X|L3],L), append(L2,L3,L1).
% -----------------------------------------------------------------

For example :

provable((p => p), Proof). % 22 inferences, 0.000 CPU in 0.000 seconds (95% CPU, 1132503 Lips) Proof = rimpl([]>[(p=>p)], ax([p]>[p], p))

But all my tentatives to get from Fitting's prover (that is complete) a prover that provides a proof like Proof above have failed. Any help that could put me on the right track would be appreciated.

CodePudding user response：

The Fitting code has some silly placement of cuts, generating spurious choice points, and an unnecessary recursion redoing all the pattern matching, instead of

directly using member/2. If you implement it more closely to the original Wang McCarthy from the LISP 1.5 Manual at page 44 ff, you get a little bit more speed:

/* Fitting */
?- time((between(1,100,_), test, fail; true)).
% 3,358,200 inferences, 0.297 CPU in 0.295 seconds (101% CPU, 11311832 Lips)
true.

/* Wang McCarthy */
?- time((between(1,100,_), test2, fail; true)).
% 2,802,900 inferences, 0.203 CPU in 0.209 seconds (97% CPU, 13798892 Lips)
true.

To arrive at Wang McCarthy replace this here from Fitting:

/* Fitting */
thm([L1|Lambda], [L2|_]) :-
        (
          L1 = L2, !
        ;
          thm(Lambda, [L2])
        ).

thm(Lambda, [~ L | Gamma]) :-
        thm([L | Lambda], Gamma), !.

thm(Lambda, [L | Gamma]) :-
        thm([~ L | Lambda], Gamma), !.

By this here:

/* Wang McCarthy */
thm2(Lambda, [L|_]) :- member(L, Lambda), !.

thm2(Lambda, [~ L | Gamma]) :- !,
        thm2([L | Lambda], Gamma).

thm2(Lambda, [L | Gamma]) :-
        thm2([~ L | Lambda], Gamma).

As a test case I was running a collection of principia mathematica tautologies.

CodePudding user response：

The following solution works smoothly and is very fast, with label for sequent rules corresponding to Fitting's sequent calculus that Fitting calls dirseq :

:- use_module(library(lists)).
:- use_module(library(statistics)).

% :- use_module(library(dom)).
% operator definitions (TPTP syntax)

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

/*
Next, a classification of formula types,
& instances.
*/

type((X & Y), conj, X, Y).
type(~((X | Y)), conj, ~ X, ~ Y).
type(~((X => Y)), conj, X, ~ Y).
type((X <=> Y), conj,  (~ X | Y),  (X | ~ Y)).
type(~((X <=> Y)), conj, (X |  Y), (~ X | ~ Y)).
type(~ (~ (X)), doub, X, _).
type((X => Y), disj, ~ X, Y).
type(~((X & Y)), disj, ~ X, ~ Y).
type((X | Y), disj, X, Y).

/*
Now the heart of the matter.
thm(Lambda, Gamma) :-
the sequent Lambda --> Gamma is provable.
*/

thm(Lambda > [Alpha | Gamma], R) :-
        type(Alpha, conj, Alpha1, Alpha2), !,
        thm(Lambda > [Alpha1 | Gamma],P), !,
        thm(Lambda > [Alpha2 | Gamma],Q),
        R = alpha(Lambda >  [Alpha | Gamma],(P & Q)).

thm(Lambda >  [Beta | Gamma], R) :-
        type(Beta, disj, Beta1, Beta2), !,
        thm(Lambda > [Beta1, Beta2 | Gamma],P),
        R = beta(Lambda >  [Beta | Gamma], P).

thm(Lambda > [Doubleneg | Gamma], R) :- 
        type(Doubleneg, doub, X, Gamma), !,
        thm(Lambda > [X | Gamma], P),
        R =  dn(Lambda > [Doubleneg | Gamma], P).

thm(Lambda > [L|Gamma], R) :-
        member(L, Lambda), !,
        R = ax(Lambda >  [L|Gamma], ax).

thm(Lambda >  [~ L | Gamma], R) :- !,
         thm([L | Lambda] >  Gamma, P),
         R = duality(Lambda >  [~ L | Gamma], P).
        
thm(Lambda > [L | Gamma], R)  :-
        thm([~ L | Lambda] >  Gamma, P),
        R = duality(Lambda > [L | Gamma], P).

/*
Finally, the driver.
*/

provable(X, R) :-
time(thm([] > [X], R)).

Many thanks for the help that I have received !