# Issue

This Content is from Stack Overflow. Question asked by Joseph Vidal-Rosset

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 P above have failed. Any help that could put me on the right road is welcome.

# Solution

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 !

``` This Question was asked in  StackOverflow by  Joseph Vidal-Rosset and Answered by Joseph Vidal-Rosset It is licensed under the terms of
CC BY-SA 2.5. - CC BY-SA 3.0. - CC BY-SA 4.0.```
people found this article helpful. What about you?