# Needing help with call_with_depth_limit/3

Hello everybody,

It is said about call_with_depth_limit/3 that

This predicate may be used for theorem provers to realise techniques like iterative deepening.

The code below is a theorem prover for classical F.O.L. that is based on Jens Otten’s work:

% ---------------------------------------------------------------------------------
% leanseq.pl - A sequent calculus prover for classical F.O.L. implemented in Prolog
% ---------------------------------------------------------------------------------

% operator definitions (TPTP syntax)

:- op( 500, fy, ~).     % negation
:- op(1000, xfy, &).    % conjunction
:- op(1100, xfy, '|').  % disjunction
:- op(1110, xfy, =>).   % conditional
:- op(1120, xfy, <=>).  % biconditional
:- op( 500, fy, !).     % universal quantifier:  ![X]:
:- op( 500, fy, ?).     % existential quantifier:  ?[X]:
:- op( 500,xfy, :).

% -----------------------------------------------------------------
decide(F) :-
prove(F,_P).
prove(F,P) :-
time(prove(F,1,P)),nl,
write('Prolog proof : '),
write(P),!.
prove(F,I,P) :-
print(iteration:I), nl,
prove([] > [F],[],I,1,_,P).
prove(F,I,P) :-
I1 is I+1,
prove(F,I1,P).
% -----------------------------------------------------------------
% THE LOGICAL RULES
% 1.The axiom
prove(G > D,_,_,J,J,ax(G>D, ax)) :-
member(A,G),
A\=(_&_), A\=(_|_), A\=(_=>_),
A\=(~_), A\=(!_), A\=(?_),
member(B,D),
unify_with_occurs_check(A,B).
% FIRST, NON-BRANCHING RULES %
%% 2. Conditional on the  right
prove(G > D,FV,I,J,K,rcond(G>D,P)) :-
select(A=>B,D,D1), !,
prove([A|G] > [B|D1],FV,I,J,K,P).
%% 3. Disjunction on the right
prove(G > D,FV,I,J,K,ror(G>D, P)) :-
select(A|B,D,D1), !,
prove(G > [A,B|D1],FV,I,J,K,P).
%% 4. Negation on the right
prove(G > D,FV,I,J,K,rneg(G>D,P)) :-
select(~A,D,D1), !,
prove([A|G] > D1,FV,I,J,K,P).
%% 5. Negation on the left
prove(G > D,FV,I,J,K,lneg(G>D,P)) :-
select(~A,G,G1), !,
prove(G1 > [A|D],FV,I,J,K,P).
%% 6. Conjunction on the left
prove(G > D,FV,I,J,K,land(G>D,P)) :-
select(A&B,G,G1), !,
prove([A,B|G1] > D,FV,I,J,K,P).
% SECOND, BRANCHING PROPOSITIONAL LOGIC RULES
% 7. Biconditional on the right
prove(G>D,FV,I,J,K, rbicond(G>D,P1,P2)):-
select((A<=>B),D,D1),!,
prove([A|G]>[B|D1],FV,I,J,J1,P1),
prove([B|G]>[A|D1],FV,I,J1,K,P2).
%% 8. Biconditional on the left
prove(G>D,FV,I,J,K, lbicond(G>D, P1,P2)):-
select((A<=>B),G,G1),!,
prove([A,B|G1]>D,FV,I,J,J1,P1),
prove(G1>[A,B|D],FV,I,J1,K,P2).
%% 9. Conditional on the left
prove(G > D,FV,I,J,K,lcond(G>D,P1,P2)) :-
select(A=>B,G,G1), !,
prove(G1 > [A|D],FV,I,J,J1,P1),
prove([B|G1] > D,FV,I,J1,K,P2).
%% 10. Conjunction on the right
prove(G > D,FV,I,J,K,rand(G>D,P1,P2)) :-
select(A&B,D,D1), !,
prove(G > [A|D1],FV,I,J,J1,P1),
prove(G > [B|D1],FV,I,J1,K,P2).
%% 11. Disjunction on the left
prove(G > D,FV,I,J,K,lor(G>D, P1,P2)) :-
select(A|B,G,G1), !,
prove([A|G1] > D,FV,I,J,J1,P1),
prove([B|G1] > D,FV,I,J1,K,P2).
%% QUANTIFICATION RULES
% 12. universal quantifier on the right
prove(G > D,FV,I,J,K,rall(G>D,P)) :-
select((![X]:A),D,D1), !,
copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
J1 is J+1,
prove(G > [A1|D1],FV,I,J1,K,P).
% 13. existential quantifier on the left
prove(G > D,FV,I,J,K,lex(G>D,P)) :-
select((?[X]:A),G,G1), !,
copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
J1 is J+1,
prove([A1|G1] > D,FV,I,J1,K,P).
% 14. existential quantifier on the right
prove(G > D,FV,I,J,K,rex(G>D,P)) :-
member((?[X]:A),D),
\+ length(FV,I),
copy_term((X:A,FV),(Y:A1,FV)),
prove(G > [A1|D],[Y|FV],I,J,K,P),!.
% 15. universal quantifier on the left
prove(G > D,FV,I,J,K,lall(G>D,P)) :-
member((![X]:A),G),
\+ length(FV,I),
copy_term((X:A,FV),(Y:A1,FV)),
prove([A1|G] > D,[Y|FV],I,J,K,P),!.

%% END of leanseq.pl code
/*
Example :

?- decide((![Y]:(f(Y)) => ![X]:(g(X))) <=> (?[Y]:(![X]:(f(Y) => g(X))))).
iteration:1
iteration:2
% 1,235 inferences, 0.001 CPU in 0.001 seconds (100% CPU, 827557 Lips)

Prolog proof : rbicond([]>[(![_18]:f(_18)=>![_20]:g(_20)<=> ?[_18]:![_20]:(f(_18)=>g(_20)))],lcond([(![_18]:f(_18)=>![_20]:g(_20))]>[?[_18]:![_20]:(f(_18)=>g(_20))],rall([]>[![_18]:f(_18),?[_18]:![_20]:(f(_18)=>g(_20))],rex([]>[f(f_sk(1,[])),?[_18]:![_20]:(f(_18)=>g(_20))],rall([]>[![_520]:(f(f_sk(1,[]))=>g(_520)),f(f_sk(1,[])),?[_18]:![_20]:(f(_18)=>g(_20))],rcond([]>[(f(f_sk(1,[]))=>g(f_sk(2,[f_sk(1,[])]))),f(f_sk(1,[])),?[_18]:![_20]:(f(_18)=>g(_20))],ax([f(f_sk(1,[]))]>[g(f_sk(2,[f_sk(1,[])])),f(f_sk(1,[])),?[_18]:![_20]:(f(_18)=>g(_20))],ax))))),rex([![_20]:g(_20)]>[?[_18]:![_20]:(f(_18)=>g(_20))],rall([![_20]:g(_20)]>[![_836]:(f(_806)=>g(_836)),?[_18]:![_20]:(f(_18)=>g(_20))],rcond([![_20]:g(_20)]>[(f(_806)=>g(f_sk(3,[_806]))),?[_18]:![_20]:(f(_18)=>g(_20))],lall([f(_806),![_20]:g(_20)]>[g(f_sk(3,[_806])),?[_18]:![_20]:(f(_18)=>g(_20))],ax([g(f_sk(3,[_806])),f(_806),![_20]:g(_20)]>[g(f_sk(3,[_806])),?[_18]:![_20]:(f(_18)=>g(_20))],ax)))))),rcond([?[_18]:![_20]:(f(_18)=>g(_20))]>[(![_18]:f(_18)=>![_20]:g(_20))],rall([![_18]:f(_18),?[_18]:![_20]:(f(_18)=>g(_20))]>[![_20]:g(_20)],lex([![_18]:f(_18),?[_18]:![_20]:(f(_18)=>g(_20))]>[g(f_sk(4,[]))],lall([![_1396]:(f(f_sk(5,[]))=>g(_1396)),![_18]:f(_18)]>[g(f_sk(4,[]))],lcond([(f(f_sk(5,[]))=>g(f_sk(4,[]))),![_1396]:(f(f_sk(5,[]))=>g(_1396)),![_18]:f(_18)]>[g(f_sk(4,[]))],lall([![_1396]:(f(f_sk(5,[]))=>g(_1396)),![_18]:f(_18)]>[f(f_sk(5,[])),g(f_sk(4,[]))],ax([f(f_sk(5,[])),![_1396]:(f(f_sk(5,[]))=>g(_1396)),![_18]:f(_18)]>[f(f_sk(5,[])),g(f_sk(4,[]))],ax)),ax([g(f_sk(4,[])),![_1396]:(f(f_sk(5,[]))=>g(_1396)),![_18]:f(_18)]>[g(f_sk(4,[]))],ax)))))))
true.

*/

Unfortunately, when formula F is invalid, we get this :

?- decide(a).
iteration:1
iteration:2
iteration:3
iteration:4
iteration:5
iteration:6
iteration:7
iteration:8
iteration:9
iteration:10
iteration:11
iteration:12
iteration:13
iteration:14
iteration:15
iteration:16
iteration:17
iteration:18
iteration:19
iteration:20
iteration:21
iteration:22
iteration:23
iteration:24
iteration:25
iteration:26
iteration:27
iteration:28
iteration:29
iteration:30
iteration:31
iteration:32
iteration:33
.
.
.

It would be a nice improvement either to limit the iteration (with call_with_depth_limit/3?, or (better), to generate a countermodel. Unfortunately, I succeed to do neither the former nor the latter.

All the best,
Jo.

PS: Once this problem solved, my goal will be to get a pretty printing with bussproofs.sty to show the output with MathJax 3.

I have checked that the antisequent trick used this prover for classical propositional logic https://vidal-rosset.net/sequent_calculus_prover_with_antisequents_for_classical_propositional_logic.html unfortunately does not work with this FOL prover.
https://www.umsu.de/trees/ also gives countermodels for invalid FOL formulas.

The other solution would be to limit the proof search with an adequate built-in predicate, like call_with_depth_limit/3 . But I did not succeed to do it.

Yes, I am aware of this point, but the first goal for me was to ban the indefinite iteration and I just thought about this solution that works, changing clauses 4 and 5 of this prover:

prove(F,I,P) :-
I < 20,
print(iteration:I), nl,
prove([] > [F],[],I,1,_,P).
prove(F,I,P) :-
I1 is I+1,
I1 < 20,
prove(F,I1,P).

It is a reasonable limit:

?- decide((![X]:(?[Y]:(f(X,Y)))) => (?[Y]:(![X]:(f(X,Y))))).
iteration:1
iteration:2
iteration:3
iteration:4
iteration:5
iteration:6
iteration:7
iteration:8
iteration:9
iteration:10
iteration:11
iteration:12
iteration:13
iteration:14
iteration:15
iteration:16
iteration:17
iteration:18
iteration:19
% 14,369,992 inferences, 1.392 CPU in 1.402 seconds (99% CPU, 10325074 Lips)
false.

Thanks for this interesting suggestion. I will try to do this.

My difficulties are more in the practice of Prolog coding than in understanding mathematical logic (here Skolem transformations).
In the same way, I met difficulties yesterday with the pretty printing to get the LaTeX bussproofs translation of the Prolog output. It works with in the propositional case, not in FOL…
About coding the Quine algorithm, I guess that this prolog program makes the job and that you know his author.

It’s good to know person interested in (deprecated ? ) call_with_depth_limit.

I found all of old Prolog codes of mine on “Ordered Linear with Ancestor resolution” prover were broken, which used the call_with_depth_limit. So I got
curious of writing a (toy) simple-minded resolution prover, which is based on:

• iterated deepening ( hand made on simple limited purpose ).

• prolog like proof search:

• topdown
• left-to-right
• history of literals relolved upon (tabling ?).

Fortunately, functionality of my old codes was
fully recovered. some example queries follows.

% Valid formula.
% ?- F = (all(y, f(y)==p) == (p==all(x, f(x)))), prove(F).
% ?- F = (((f(1)==p) & (f(2) == p)) == (p== (f(1) & f(2)))), prove(F).
% ?- F = (all(A, p==f(A))==(p==all(B, f(B)))), prove(F).
% ?- F = ((p == all(A, f(A))) == all(B, p== f(B))), prove(F).
% ?- F = ((p == all(A, f(A))) -> all(B, p -> f(B))), prove(F).
% ?- F = ((p == all(A, f(A))) -> all(B, f(B) -> p)), prove(F).
% ?- F = ((p == all(A, f(A))) -> all(B, p -> f(B))), prove(F).
% ?- F = ((p == all(A, f(A))) -> all(B, f(B) -> p)), prove(F).

% Invalid formula.
% ?- prove(all(y, some(x, f(x, y)) -> some(x, all(y, f(x, y))))). % false
% ?- prove((all(X, some(Y, p(X, Y)))->some(Y, all(X, p(X, Y))))).  % false.
% ?- prove((some(X, p(X))->all(X, p(X)))).		% false.

However new codes lacks anything like paramodulation strategy, for which
I have no idea (sigh). So, to prove properties on functions on natural number, for example, it must be very weak.

BTW, I have tried to upload my pack pac as v1.8.9 with this new codes, but failed. It seems that packages manager has been changed.

This is actually on the way, not yet 100% done, but very promising already.

This misunderstanding is explained by the fact that Skolem function are also used in Jens Otten’s prover:

rules for Eigenvariables using Skolemization [rules E left and A right]

But seqprover.pl , the classical sequent calculus prover (akin to LK) by Naoyuki Tamura Naoyuki Tamura maybe fits with your point of view. See its code where ground/1 is used.

I feel free to paste seqprover.pl here, even if it contains many lines of Prolog code. It works perfectly with SWI Prolog. The LaTeX macro that is used is proof.sty but it is probably possible to rewrite this part to use bussproofs.sty instead.

%%%
%%%  Sequent Calculus Prover in Prolog
%%%  by Naoyuki Tamura (tamura@kobe-u.ac.jp)
%%%  TeX form output by Eiji Sugiyama
%%%
%%%  You can freely distribute or modify this program.
%%%
%%%  Version 2.0
%%%    12/30/2020 Modified for SWI Prolog
%%%
:- dynamic
seq_system/2, threshold/1, output_form/1, logging/2,
output_count/1, output_result/2,
proved/3, not_proved/2, axiom/1.
%seq_system(cl,first).
%threshold(5).
%output_form(pretty).
%logging(no, _).
%output_count(1).

:- op(1200, xfx, [ -->, <--> ]).
:- op( 900, xfy, [ -> ]).
% :- op( 850, xfy, [ -> ]).
:- op( 850, xfy, [ /\, \/ ]).
:- op( 800, fy,  [ ~ ]).
:- op( 750, xfy, [ @, # ]).

prover :-
writex('Sequent Calculus Prover ver 2.0 in Prolog'), nlx,
writex('        by Naoyuki Tamura (tamura@kobe-u.ac.jp)'), nlx,
%	seq_init,
statistics(runtime, [T0,_]),
seq_prover,
statistics(runtime, [T1,_]),
T is T1-T0,
writex('Exit from Sequent Calculus Prover...'), nlx,
writex('Total CPU time = '), writex(T), writex(' msec.'), nlx,
log_end.

seq_init :-
set_system(cl,first),
set_threshold(5),
set_axioms([]),
set_output_form(pretty),
log_end,
reset_output_result.

seq_prover :-
current_input(STR),
seq_prover(STR).

seq_prover(STR) :-
prompt(_, ''),
repeat,
seq_system(Sys, Opt),
writex(Sys), writex('('), writex(Opt), writex(')'),
writex('> '),
flush_out,
seq_command(X),
seq_quit(X),
close(STR).

seq_quit(X) :-
nonvar(X),
memberq(X, [quit, end, bye, halt, end_of_file]).

seq_command(X) :-
seq_execute(X),
!,
writex(yes), nlx.
seq_command(_) :-
writex(no), nlx.

seq_execute(X) :- var(X), !, fail.
seq_execute(X) :- seq_quit(X), !.
seq_execute(help) :- !, seq_help.
seq_execute(init) :- !, seq_init.
seq_execute([File]) :- !, seq_consult(File).
seq_execute(cl(Opt)) :- !, set_system(cl,Opt).
%seq_execute(il(Opt)) :- !, set_system(il,Opt).
seq_execute(threshold(N)) :- var(N), !,
threshold(N),
writex(threshold(N)), nlx.
seq_execute(threshold(N)) :- !,
set_threshold(N).
seq_execute(axioms(As)) :- var(As), !,
(bagof(A, axiom(([]-->[A])), As); As=[]), !,
writex(axioms(As)), nlx.
seq_execute(axioms(As)) :- !,
set_axioms(As).
seq_execute(output(Form)) :- var(Form), !,
output_form(Form),
writex(output(Form)), nlx.
seq_execute(output(Form)) :-
set_output_form(Form).
seq_execute(log(File)) :- var(File), !,
logging(File, _),
writex(log(File)), nlx.
seq_execute(log(no)) :- !,
log_end.
seq_execute(log(File)) :- !,
log_start(File).
seq_execute(N) :- integer(N), !,
get_output_result(N, N1, P),
print_output(N1, P).
seq_execute((Xs <--> Ys)) :- !,
seq_execute((Xs --> Ys)),
seq_execute((Ys --> Xs)).
seq_execute((Xs --> Ys)) :-
convert_to_seq((Xs --> Ys), Seq),
sequentq(Seq),
!,
seq_prove(Seq).
seq_execute(X) :-
writex('Error '),
writex(X),
writex(' is not a command nor a sequent.'), nlx.

seq_help :-
writex('A1,...,Am -->  B1,...,Bn : Try to prove the sequent.'), nlx,
writex('A1,...,Am <--> B1,...,Bn : Try to prove the sequent '),
writex('in both directions.'), nlx,
writex('help           : Help.'), nlx,
writex('init           : Initialize the prover.'), nlx,
writex('[File]         : Read from the file.'), nlx,
writex('Sys(Opt)       : Select the system. '),
writex('Sys={cl}, Opt={first|prop}'), nlx,
writex('threshold(N)   : Set/retrieve the threshold. N>=0'), nlx,
writex('axioms(Axioms) : Set/retrieve the axioms. '),
writex('Axioms=[A1,...,Am]'), nlx,
writex('output(Form)   : Set/retrieve the output form. '),
writex('Form={pretty|tex|standard|term}'), nlx,
writex('log(L)         : Start/stop/retrieve the output logging. '),
writex('L={yes|File|no}'), nlx,
writex('N              : Display the N-th output.'), nlx,
writex('quit           : Quit.'), nlx.

seq_consult(File) :-
seq_prover(STR).

seq_prove(Seq) :-
statistics(runtime,[_,_]),
prove(Seq, Proof),
statistics(runtime,[_,Time]),
writex('Succeed in proving '),
write_seq(Seq),
writex(' ('), writex(Time), writex(' msec.)'), nlx,
output_count(N),
assert_output_result(Proof),
!,
print_output(N, Proof).
seq_prove(Seq) :-
statistics(runtime,[_,Time]),
writex('Fail to prove '),
write_seq(Seq),
writex(' ('), writex(Time), writex(' msec.)'), nlx.

print_output(N, P) :-
output_form(Form), writex(Form), writex(':'),
writex(N), writex(' ='), nlx,
print_proof(P).

print_proof(P) :-
output_form(Form),
print_proof_form(Form, P).

print_proof_form(pretty, P) :- !,
pretty_print(P).
print_proof_form(tex, P) :- !,
tex_print(P).
print_proof_form(standard, P) :- !,
standard_print(P).
print_proof_form(term, P) :- !,
writex(P), nlx.

set_system(Sys, Opt) :-
memberq(Sys, [cl]),
memberq(Opt, [prop,first]),
retractall(seq_system(_,_)),
assert(seq_system(Sys,Opt)).

set_threshold(N) :-
integer(N), N >= 0,
retractall(threshold(_)),
assert(threshold(N)).

set_axioms(Axioms) :-
retractall(axiom(_)),
assert_axioms(Axioms).

assert_axioms([]).
assert_axioms([A|As]) :-
formulaq(A),
!,
assert(axiom(([]-->[A]))),
assert_axioms(As).
assert_axioms([A|As]) :-
writex('Error '), writex(A),
writex(' is not a formula.'), nlx,
assert_axioms(As).

set_output_form(Form) :-
memberq(Form, [pretty, tex, standard, term]),
retractall(output_form(_)),
assert(output_form(Form)).

reset_output_result :-
retractall(output_count(_)),
retractall(output_result(_,_)),
assert(output_count(1)).

assert_output_result(P) :-
output_count(N),
assert(output_result(N,P)),
retractall(output_count(_)),
N1 is N+1,
assert(output_count(N1)).

get_output_result(N, N, P) :- N>0, !,
output_result(N, P).
get_output_result(N, N1, P) :-
output_count(M),
N1 is M+N,
output_result(N1, P).

convert_to_seq((Xs --> Ys), (Xs1 --> Ys1)) :-
convert_to_list(Xs, Xs1), convert_to_list(Ys, Ys1).

convert_to_list(X, _) :- var(X), !, fail.
convert_to_list([], []) :- !.
convert_to_list([X|Xs], [X|Xs]) :- !.
convert_to_list((X,Xs), [X|Zs]) :- !, convert_to_list(Xs, Zs).
convert_to_list(X, [X]).

sequentq((X-->Y)) :- formula_listq(X), formula_listq(Y).

formula_listq([]).
formula_listq([A|As]) :- formulaq(A), formula_listq(As).

formulaq(A) :- var(A), !, fail.
formulaq((_-->_)) :- !, fail.
formulaq([]) :- !, fail.
formulaq([_|_]) :- !, fail.
formulaq(~A) :- !, formulaq(A).
formulaq(A/\B) :- !, formulaq(A), formulaq(B).
formulaq(A\/B) :- !, formulaq(A), formulaq(B).
formulaq(A->B) :- !, formulaq(A), formulaq(B).
formulaq(_X@A) :- !, formulaq(A).
formulaq(_X#A) :- !, formulaq(A).
formulaq(_).

%%
%%  Sequent Calculus Prover
%%
%%  seq_system( {cl}, {prop|first} ).
%%    seq_system(cl,first).
%%  Max number of cut and contraction rules: cut, r(all), l(exists)
%%    threshold(5).
%%  Axioms
%%    axiom(Ax1). axiom(Ax2). ....

prove(S, P) :-
retractall(proved(_,_,_)),
retractall(not_proved(_,_)),
threshold(N),
writex('Trying to prove with threshold ='),
for(I, 0, N),
writex(' '), writex(I),
flush_out,
prove(S, P, I),
nlx,
!.
prove(_S, _P) :-
nlx,
fail.

prove(S, _P, N) :-
ground(S),
clause(not_proved(S,M), _),
N =< M,
!,
fail.
prove(S, P, N) :-
ground(S),
clause(proved(S,P,M), _),
M =< N,
!.
prove(S, P, _N) :-
clause(axiom(S), _),
P = [axiom,[[]],S],
!.
prove(S, P, N) :-
check_sequent(S),
select_rule(Rule, S, Ss, Pos),
P = [Rule,Pos,S|Ps],
set_sequents(Ss, Ps),
rule_constraint(Rule, Ps, M),
N1 is N-M, N1 >= 0,
prove_all(Ss, Ps, N1),
%	!,
assert(proved(S,P,N)).
prove(S, _P, N) :-
ground(S),
assert(not_proved(S,N)),
!,
fail.

prove_all([], [], _N).
prove_all([S|Ss], [P|Ps], N) :-
prove(S, P, N),
prove_all(Ss, Ps, N).

check_sequent((X-->Y)) :-
length(X, N1), length(Y, N2),
N1 + N2 < 20.
%check_sequent(_) :- seq_system(cl,_), !.
%check_sequent((_X-->Y)) :- (Y=[]; Y=[_]), !.

select_rule(Rule, S, Ss, Pos) :-
rule(RuleSys, inv, Rule, S, Ss, Pos),
check_rule(RuleSys),
!.
select_rule(Rule, S, Ss, Pos) :-
rule(RuleSys, no, Rule, S, Ss, Pos),
check_rule(RuleSys).

check_rule([RSys,ROp]) :-
seq_system(Sys, Op),
check_rule1(Sys, RSys),
check_rule2(Op, ROp),
!.

check_rule1(Sys, Sys).
check_rule1(cl, _).

check_rule2(Op, Op).
check_rule2(first, _).

set_sequents([], []).
set_sequents([S|Ss], [[_,_,S|_]|Ps]) :- set_sequents(Ss, Ps).

rule_constraint(cut, [P1,_P2], 1) :- !,
axiom(S1),
P1 = [axiom,_,S1].
% bug report from Joseph Vidal-Rosset
rule_constraint(l(all), [P1], 1) :- !,
P1 = [NextRule,_,_|_],
dif(NextRule, l(all)).
rule_constraint(r(exists), [P1], 1) :- !,
P1 = [NextRule,_,_|_],
dif(NextRule, r(exists)).
rule_constraint(_Rule, _, 0).

% Logical axiom
% cannot be invertible owing to unification
rule([cl,prop], no, ax, S, [], [[]]) :-
match(S,  ([_X1,[A],_X2]-->[_Y1,[A],_Y2])).
% Rules for the propositional constants
rule([cl,prop], inv, l(top), S, [S1], [l(N),[]]) :-
match(S,  ([X1,[top],X2]-->[Y])),
match(S1, ([X1,X2]-->[Y])),
length(X1, N).
rule([cl,prop], inv, r(top), S, [], [r(N)]) :-
match(S,  ([_X]-->[Y1,[top],_Y2])),
length(Y1, N).
rule([cl,prop], inv, l(bot), S, [], [r(N)]) :-
match(S,  ([X1,[bot],_X2]-->[_Y])),
length(X1, N).
rule([cl,prop], inv, r(bot), S, [S1], [r(N),[]]) :-
match(S,  ([X]-->[Y1,[bot],Y2])),
match(S1, ([X]-->[Y1,Y2])),
length(Y1, N).
% Rules for the propositional connectives
rule([cl,prop], inv, l(~), S, [S1], [l(N),r(0)]) :-
match(S,  ([X1,[(~A)],X2]-->[Y])),
match(S1, ([X1,X2]-->[[A],Y])),
length(X1, N).
rule([cl,prop], inv, r(~), S, [S1], [r(N),l(0)]) :-
match(S,  ([X]-->[Y1,[~A],Y2])),
match(S1, ([[A],X]-->[Y1,Y2])),
length(Y1, N).
rule([cl,prop], inv,  l(/\), S, [S1], [l(N),[l(N),l(N1)]]) :-
match(S,  ([X1,[A/\B],X2]-->[Y])),
match(S1, ([X1,[A,B],X2]-->[Y])),
length(X1, N), N1 is N+1.
rule([cl,prop], inv,  r(\/), S, [S1], [r(N),[r(N),r(N1)]]) :-
match(S,  ([X]-->[Y1,[A\/B],Y2])),
match(S1, ([X]-->[Y1,[A,B],Y2])),
length(Y1, N), N1 is N+1.
rule([cl,prop], inv, r(->), S, [S1], [r(N),[l(0),r(N)]]) :-
match(S,  ([X]-->[Y1,[A->B],Y2])),
match(S1, ([[A],X]-->[Y1,[B],Y2])),
length(Y1, N).
rule([cl,prop], inv, r(/\), S, [S1, S2], [r(N),r(N),r(N)]) :-
match(S,  ([X]-->[Y1,[A/\B],Y2])),
match(S1, ([X]-->[Y1,[A],Y2])),
match(S2, ([X]-->[Y1,[B],Y2])),
length(Y1, N).
rule([cl,prop], inv, l(\/), S, [S1, S2], [l(N),l(N),l(N)]) :-
match(S,  ([X1,[A\/B],X2]-->[Y])),
match(S1, ([X1,[A],X2]-->[Y])),
match(S2, ([X1,[B],X2]-->[Y])),
length(X1, N).
rule([cl,prop], inv,  l(->), S, [S1, S2], [l(N),r(0),l(N)]) :-
match(S,  ([X1,[A->B],X2]-->[Y])),
match(S1, ([X1,X2]-->[[A],Y])),
match(S2, ([X1,[B],X2]-->[Y])),
length(X1, N).
% Rules for the quantifiers
rule([cl,first], no,  l(all), S, [S1], [l(N),[l(N),l(N1)]]) :-
match(S,  ([X1,[V@A],X2]-->[Y])),
substitute(V, _V1, A, A1),
match(S1, ([X1,[A1,V@A],X2]-->[Y])),
length(X1, N), N1 is N+1.
rule([cl,first], no, r(all), S, [S1], [r(N),r(N)]) :-
match(S,  ([X]-->[Y1,[V@A],Y2])),
substitute(V, V1, A, A1),
match(S1, ([X]-->[Y1,[A1],Y2])),
eigen_variable(V1, S),
length(Y1, N).
rule([cl,first], no, l(exists), S, [S1], [l(N),l(N)]) :-
match(S,  ([X1,[V#A],X2]-->[Y])),
substitute(V, V1, A, A1),
match(S1, ([X1,[A1],X2]-->[Y])),
eigen_variable(V1, S),
length(X1, N).
rule([cl,first], no,  r(exists), S, [S1], [r(N),[r(N),r(N1)]]) :-
match(S,  ([X]-->[Y1,[V#A],Y2])),
substitute(V, _V1, A, A1),
match(S1, ([X]-->[Y1,[A1,V#A],Y2])),
length(Y1, N), N1 is N+1.
% Cut rule
rule([cl,prop], no,  cut, S, [S1, S2], [[],r(0),l(0)]) :-
match(S,  ([X]-->[Y])),
match(S1, ([]-->[[C]])),
match(S2, ([[C],X]-->[Y])).

match((X-->Y), (P-->Q)) :- append_all(P, X), append_all(Q, Y).

eigen_variable(V, X) :-
freeze(V, fail),
free_variables(X, Us),
dif_list(Us, V).

free_variables(X, Vs) :- free_vars(X, [], [], Vs).

free_vars(X, BVs, Vs0, Vs) :- var(X), !, free_vars1(X, BVs, Vs0, Vs).
free_vars(X, _BVs, Vs, Vs) :- ground(X), !.
free_vars([X|Y], BVs, Vs0, Vs) :- !,
free_vars(X, BVs, Vs0, Vs1), free_vars(Y, BVs, Vs1, Vs).
free_vars(all(X,A), BVs, Vs0, Vs) :- !,
free_vars(A, [X|BVs], Vs0, Vs).
free_vars(exists(X,A), BVs, Vs0, Vs) :- !,
free_vars(A, [X|BVs], Vs0, Vs).
free_vars(X, BVs, Vs0, Vs) :- X =.. Y, free_vars(Y, BVs, Vs0, Vs).

free_vars1(X, BVs, Vs, Vs) :- (memq(X, BVs); memq(X, Vs)), !.
free_vars1(X, _BVs, Vs, [X|Vs]).

dif_list([], _).
dif_list([U|Us], V) :- dif(U, V), dif_list(Us, V).

%%
%%  Standard form printer
%%
standard_print(P) :-
standard_print(P, 0).

standard_print([Rule,_,S|Ps], Tab) :-
tabx(Tab),
write_rule_name(Rule), writex(': '),
write_seq(S), nlx,
Tab1 is Tab+2,
standard_print_list(Ps, Tab1).

standard_print_list([], _).
standard_print_list([P|Ps], Tab) :-
standard_print(P, Tab), standard_print_list(Ps, Tab).

%%
%%  Pretty form printer
%%
pretty_print(P0) :-
name_variables(P0, P),
place_proof(P, [], Q, _, _),
print_placed_proof(Q),
fail.
pretty_print(_).

name_variables(X, Z) :-
name_variables(X, 0, _N, [], _Vs, Z).

name_variables(X, N, N, Vs, Vs, X) :- ground(X), !.
name_variables(X, N, N, Vs, Vs, Z) :- var(X), assoc(X, Z, Vs), !.
name_variables(X, N0, N, Vs0, [[X|Z]|Vs0], Z) :- var(X), !,
V is N0 mod 3, VN is N0//3,
name_var(V, VN, Z),
N is N0+1.
name_variables([X|Xs], N0, N, Vs0, Vs, [Z|Zs]) :- !,
name_variables(X, N0, N1, Vs0, Vs1, Z),
name_variables(Xs, N1, N, Vs1, Vs, Zs).
name_variables(X, N0, N, Vs0, Vs, Z) :-
X =.. Xs,
name_variables(Xs, N0, N, Vs0, Vs, Zs),
Z =.. Zs.

name_var(0, VN, X) :- !, name_var1([0'X], VN, X).
name_var(1, VN, X) :- !, name_var1([0'Y], VN, X).
name_var(2, VN, X) :- !, name_var1([0'Z], VN, X).

name_var1([V], 0, X) :- !, name(X, [V]).
name_var1([V], VN, X) :-
name(VN, Ns),
name(X, [V|Ns]).

%%
%%  place_proof(+Proof, +Margins,
%%              -Proof_with_pos, -LowerLeftPos, -NewMargins)
%%
place_proof([Rule,_,S|Ps1], Ms0, Q, LowerPos, Ms) :-
get_margins([M0,M1|Ms1], Ms0),
place_uppers(Ps1, Ms1, Ps2, UpperPos0, Ms2),
get_margins([M2|_], Ms2),
UpperWidth is M2-UpperPos0,
get_rule_name_width(Rule, W1),
get_seq_width(S, LowerWidth),
LowerOff is max(0,max(UpperPos0,max(M1,M0))-UpperPos0),
RulePos is UpperPos0+LowerOff,
RuleWidth is max(UpperWidth,LowerWidth),
LowerPos is RulePos+(RuleWidth-LowerWidth)//2,
UpperPos is max(UpperPos0,RulePos),
UpperOff is UpperPos-UpperPos0,
move_proof_list(Ps2, UpperOff, Ps3),
move_margins(Ms2, UpperOff, Ms3),
new_rule_width(Rule, RuleWidth, W1, RuleWidth1, W2),
Q = [RulePos+RuleWidth1,Rule,LowerPos+LowerWidth,S|Ps3],
M11 is RulePos+RuleWidth1+W2,
M01 is LowerPos+LowerWidth,
Ms = [M01,M11|Ms3].

new_rule_width([_Rule,_], _, W1, 0, W1) :- !.
new_rule_width(_Rule, RW, W1, RW, W2) :- W2 is W1+1.

place_uppers(Ps, Ms0, Qs, T, Ms) :-
place_proof_list(Ps, Ms0, Qs, T, Ms).

place_proof_list([], Ms0, [], T, Ms0) :- !,
get_margins([T|_], Ms0).
place_proof_list([P1], Ms0, [Q1], T, Ms) :- !,
place_proof(P1, Ms0, Q1, T, Ms).
place_proof_list([P1|Ps], Ms0, [Q1|Qs], T, Ms) :-
place_proof(P1, Ms0, Q1, T, Ms1),
move_margins(Ms1, 2, Ms2),
place_proof_list(Ps, Ms2, Qs, _T1, Ms).

move_proof_list([], _, []).
move_proof_list([P0|Ps0], Off, [P|Ps]) :-
move_proof(P0, Off, P),
move_proof_list(Ps0, Off, Ps).

move_proof([M0+W0,Rule,M1+W1,S|Ps0], Off, [N0+W0,Rule,N1+W1,S|Ps]) :-
N0 is M0+Off, N1 is M1+Off,
move_proof_list(Ps0, Off, Ps).

get_margins(Zs, Xs) :- var(Zs), !, Zs=Xs.
get_margins([], _).
get_margins([Z|Zs], []) :- !, Z=0, get_margins(Zs, []).
get_margins([Z|Zs], [Z|Xs]) :- get_margins(Zs, Xs).

move_margins([], _, []).
move_margins([M0|Ms0], Off, [M|Ms]) :-
M is M0+Off, move_margins(Ms0, Off, Ms).

%%
%%  print_placed_proof(+Placed_Proof)
%%
print_placed_proof(P) :-
print_placed_proofs([P]).

print_placed_proofs([]).
print_placed_proofs(Ps) :- Ps=[_|_],
gather_uppers(Ps, Qs),
print_placed_proofs(Qs),
print_rules(Ps),
nlx,
print_lowers(Ps),
nlx.

gather_uppers([], []).
gather_uppers([P|Ps], Qs) :-
gather_uppers(Ps, Qs1),
P = [_,_Rule,_,_S|P0],
append(P0, Qs1, Qs).

print_rules([]).
print_rules([P|Ps]) :-
P = [M0+W0,Rule,_M1+_W1,_S|_],
goto_pos(M0),
print_rule_line(W0),
write_rule_name(Rule),
print_rules(Ps).

print_rule_line(0) :- !.
print_rule_line(N) :- N>0, n_writex(N, '-'), writex(' ').

print_lowers([]).
print_lowers([P|Ps]) :-
P = [_M0+_W0,_Rule,M1+_W1,S|_],
goto_pos(M1),
write_seq(S),
print_lowers(Ps).

get_width(X, W) :-
open_null(NULL, OldSTR, OldLog),
nlx,
writex(X),
line_position(W),
close_null(NULL, OldSTR, OldLog).

get_rule_name_width(R, W) :-
open_null(NULL, OldSTR, OldLog),
nlx,
write_rule_name(R),
line_position(W),
close_null(NULL, OldSTR, OldLog).

get_seq_width(S, W) :-
open_null(NULL, OldSTR, OldLog),
nlx,
write_seq(S),
line_position(W),
close_null(NULL, OldSTR, OldLog).

open_null(NULL, OldSTR, OldLog) :-
current_output(OldSTR),
open_null_stream(NULL),
set_output(NULL),
log_suspend(OldLog).

close_null(NULL, OldSTR, OldLog) :-
close(NULL),
set_output(OldSTR),
log_resume(OldLog).

write_rule_name(axiom) :- !, writex('Axiom').
write_rule_name(ax) :- !, writex('Ax').
write_rule_name(cut) :- !, writex('Cut').
write_rule_name(r(all)) :- !, writex('R@').
write_rule_name(r(exists)) :- !, writex('R#').
write_rule_name(r(R)) :- !, writex('R'), writex(R).
%write_rule_name(r(R,N)) :- !, writex('R'), writex(R), writex(N).
write_rule_name(l(all)) :- !, writex('L@').
write_rule_name(l(exists)) :- !, writex('L#').
write_rule_name(l(R)) :- !, writex('L'), writex(R).
%write_rule_name(l(R,N)) :- !, writex('L'), writex(R), writex(N).

write_seq((Xs-->Ys)) :-
write_list(Xs), writex(' --> '), write_list(Ys).

write_list([]).
write_list([X]) :- !, writex(X).
write_list([X|Xs]) :- writex(X), writex(','), write_list(Xs).

%%
%%  Tex form printer
%%
tex_print(P) :-
tex_name_variables(P, Q),
tex_print(0, Q).

tex_name_variables(X, Z) :-
tex_name_variables(X, 0, _N, [], _Vs, Z).

tex_name_variables(X, N, N, Vs, Vs, X) :- ground(X), !.
tex_name_variables(X, N, N, Vs, Vs, Z) :- var(X), assoc(X, Z, Vs), !.
tex_name_variables(X, N0, N, Vs0, [[X|Z]|Vs0], Z) :- var(X), !,
V is N0 mod 3, VN is N0//3,
tex_name_var(V, VN, Z),
N is N0+1.
tex_name_variables([X|Xs], N0, N, Vs0, Vs, [Z|Zs]) :- !,
tex_name_variables(X, N0, N1, Vs0, Vs1, Z),
tex_name_variables(Xs, N1, N, Vs1, Vs, Zs).
tex_name_variables(X, N0, N, Vs0, Vs, Z) :-
X =.. Xs,
tex_name_variables(Xs, N0, N, Vs0, Vs, Zs),
Z =.. Zs.

tex_name_var(0, VN, X) :- !, tex_name_var1([0'x], VN, X).
tex_name_var(1, VN, X) :- !, tex_name_var1([0'y], VN, X).
tex_name_var(2, VN, X) :- !, tex_name_var1([0'z], VN, X).

tex_name_var1([V], 0, X) :- !, name(X, [V]).
tex_name_var1([V], VN, X) :-
name(VN, Ns), append(Ns, [0'}], Ns1),
name(X, [V,0'_,0'{|Ns1]).

tex_print(Tab, [[Rule,LN],_,S]) :- !,
tabx(Tab), writex('\\deduce{'),
tex_print_sequent(S), writex('}{'),
tex_print_rule_name([Rule,LN]),	writex('}'), nlx.
tex_print(Tab, [Rule,_,S]) :- (Rule = ax; Rule = axiom), !,
tabx(Tab), tex_print_sequent(S).
tex_print(Tab, [Rule,_,S|Ss]) :-
tabx(Tab), writex('\\infer['),
tex_print_rule_name(Rule), writex(']{'),
tex_print_sequent(S),
writex('}{'),
tex_print_list(Ss, Tab),
writex('}'), nlx.

tex_print_list([], _Tab).
tex_print_list([S1], Tab) :- !,
nlx,
Tab1 is Tab+2,
tex_print(Tab1, S1),
tabx(Tab).
tex_print_list([S1|Ss], Tab) :- !,
nlx,
Tab1 is Tab+2,
tex_print(Tab1, S1),
tabx(Tab1), writex('&'),
tex_print_list(Ss, Tab).

tex_print_sequent((Xs-->Ys)) :-
tex_print_formulas(Xs),
writex(' \\lra '),
tex_print_formulas(Ys).

tex_print_formulas([]).
tex_print_formulas([A]) :- !,
tex_print_formula(A).
tex_print_formulas([A|As]) :-
tex_print_formula(A),
writex(', '),
tex_print_formulas(As).

tex_print_formula(A) :-
tex_print_formula(999, A).

tex_print_formula(Prec0, A) :- tex_quantifier_name(A, Q, X, B), !,
Prec = 999,
(Prec0 < Prec -> writex('('); true),
writex(Q), writex(' '), writex(X), writex('.'),
tex_print_formula(B),
(Prec0 < Prec -> writex(')'); true),
!.
tex_print_formula(Prec0, A) :- is_op(A, Prec, Type, Op, As), !,
(Prec0 < Prec -> writex('('); true),
tex_print_op_formula(Prec, Type, Op, As),
(Prec0 < Prec -> writex(')'); true),
!.
tex_print_formula(_Prec0, A) :- tex_unit_name(A, U), !,
writex(U).
tex_print_formula(_Prec0, A) :-
rename_functor(A, A1),
writex(A1).

rename_functor(X, Z) :-
X =.. [F0|As],
capitalize_atom(F0, F),
Z =.. [F|As].

tex_quantifier_name(X@A, '\\forall', X, A).
tex_quantifier_name(X#A, '\\exists', X, A).

tex_unit_name(_, _) :- fail.
tex_unit_name(bot, '\\bot').
tex_unit_name(top, '\\top').

%tex_print_op_formula(Prec, fy, Op, [A1]) :- Op = ~, !,
%	tex_print_op(Op), writex('{'),
%	tex_print_formula(Prec, A1), writex('}').
tex_print_op_formula(Prec, fx, Op, [A1]) :- !,
Prec1 is Prec - 1,
tex_print_op(Op), writex(' '),
tex_print_formula(Prec1, A1).
tex_print_op_formula(Prec, fy, Op, [A1]) :- !,
tex_print_op(Op), writex(' '),
tex_print_formula(Prec, A1).
tex_print_op_formula(Prec, xf, Op, [A1]) :- !,
Prec1 is Prec - 1,
tex_print_formula(Prec1, A1),
writex(' '), tex_print_op(Op).
tex_print_op_formula(Prec, yf, Op, [A1]) :- !,
tex_print_formula(Prec, A1),
writex(' '), tex_print_op(Op).
tex_print_op_formula(Prec, xfx, Op, [A1,A2]) :- !,
Prec1 is Prec - 1,
tex_print_formula(Prec1, A1),
writex(' '), tex_print_op(Op), writex(' '),
tex_print_formula(Prec1, A2).
tex_print_op_formula(Prec, xfy, Op, [A1,A2]) :- !,
Prec1 is Prec - 1,
tex_print_formula(Prec1, A1),
writex(' '), tex_print_op(Op), writex(' '),
tex_print_formula(Prec, A2).
tex_print_op_formula(Prec, yfx, Op, [A1,A2]) :- !,
Prec1 is Prec - 1,
tex_print_formula(Prec, A1),
writex(' '), tex_print_op(Op), writex(' '),
tex_print_formula(Prec1, A2).

is_op(A, Prec, Type, Op, As) :-
functor(A, Op, N), current_op(Prec, Type, Op),
is_op0(A, Type, N, As),
!.
is_op0(A, fx, 1, [A1]) :- arg(1, A, A1).
is_op0(A, fy, 1, [A1]) :- arg(1, A, A1).
is_op0(A, xf, 1, [A1]) :- arg(1, A, A1).
is_op0(A, yf, 1, [A1]) :- arg(1, A, A1).
is_op0(A, xfx, 2, [A1,A2]) :- arg(1, A, A1), arg(2, A, A2).
is_op0(A, xfy, 2, [A1,A2]) :- arg(1, A, A1), arg(2, A, A2).
is_op0(A, yfx, 2, [A1,A2]) :- arg(1, A, A1), arg(2, A, A2).

tex_print_op(Op) :-
tex_op_name(Op, OpName), !,
writex(OpName).

tex_op_name(~,  '\\lnot').
tex_op_name(/\, '\\land').
tex_op_name(\/, '\\lor').
tex_op_name(->, '\\imp').

tex_print_rule_name([Rule,LN]) :- !,
tex_rule_name(Rule, RuleName),
!,
writex(RuleName),
writex('('), writex(LN), writex(')').
tex_print_rule_name(Rule) :-
tex_rule_name(Rule, RuleName),
!,
writex(RuleName).

tex_rule_name(ax, '({\\rm Ax})').
tex_rule_name(axiom, '({\\rm Axiom})').
tex_rule_name(l(top), '({\\rm L}\\top)').
tex_rule_name(r(top), '({\\rm R}\\top)').
tex_rule_name(l(bot), '({\\rm L}\\bot)').
tex_rule_name(r(bot), '({\\rm R}\\bot)').
tex_rule_name(l(~), '({\\rm L}\\lnot)').
tex_rule_name(r(~), '({\\rm R}\\lnot)').
tex_rule_name(l(/\), '({\\rm L}\\land)').
tex_rule_name(r(/\), '({\\rm R}\\land)').
tex_rule_name(l(\/), '({\\rm L}\\lor)').
tex_rule_name(r(\/), '({\\rm R}\\lor)').
tex_rule_name(l(->), '({\\rm L}\\imp)').
tex_rule_name(r(->), '({\\rm R}\\imp)').
tex_rule_name(l(all), '({\\rm L}\\forall)').
tex_rule_name(r(all), '({\\rm R}\\forall)').
tex_rule_name(l(exists), '({\\rm L}\\exists)').
tex_rule_name(r(exists), '({\\rm R}\\exists)').
tex_rule_name(cut, '({\\rm Cut})').

%%
%%  Utilities
%%
append_all([], []).
append_all([P], P).
append_all([P|Ps], X) :- Ps=[_|_], append(P, X1, X), append_all(Ps, X1).

merge(X1, X2, X) :- split(X, X1, X2).

split([], [], []).
split([X|Xs], [X|Ys], Zs) :- split(Xs, Ys, Zs).
split([X|Xs], Ys, [X|Zs]) :- split(Xs, Ys, Zs).

append([], Z, Z).
append([W|X], Y, [W|Z]) :- append(X, Y, Z).

member(X, [X|_Xs]).
member(X, [_Y|Xs]) :- member(X, Xs).

memberq(X, [X|_Xs]) :- !.
memberq(X, [_Y|Xs]) :- memberq(X, Xs).

memq(X, [Y|_Xs]) :- X==Y, !.
memq(X, [_Y|Xs]) :- memq(X, Xs).

get_nth(0, [X|_Xs], X) :- !.
get_nth(N, [_|Xs], X) :- N>0, N1 is N-1, get_nth(N1, Xs, X).

for(I, M, N) :- M =< N, I=M.
for(I, M, N) :- M =< N, M1 is M+1, for(I, M1, N).

assoc(X, Z, [[X0|Z]|_As]) :- X==X0, !.
assoc(X, Z, [_|As]) :- assoc(X, Z, As).

substitute(X0, X, A0, A) :- var(A0), X0==A0, !, A=X.
substitute(_X0, _X, A0, A) :- var(A0), !, A=A0.
substitute(_X0, _X, A0, A) :- atomic(A0), !, A=A0.
substitute(X0, X, [A0|B0], [A|B]) :- !,
substitute(X0, X, A0, A),
substitute(X0, X, B0, B).
substitute(X0, X, A0, A) :-
A0 =.. B0,
substitute(X0, X, B0, B),
A =.. B.

capitalize_atom(X, Z) :- atom(X),
name(X, [C0|Cs]), C0 >= 0'a, C0 =< 0'z, !,
C is ((C0 - 0'a) + 0'A),
name(Z, [C|Cs]).
capitalize_atom(X, X).

n_writex(0, _) :- !.
n_writex(N, X) :- N>0, writex(X), N1 is N-1, n_writex(N1, X).

flush_out :-
current_output(S),
flush_output(S).

goto_pos(T) :-
current_output(S),
line_position(S, T0),
tabx(T-T0).

line_position(W) :-
current_output(S),
line_position(S, W).

%%
%%  Logging
%%
log_start(yes) :- !,
log_start('seqprover.log').
log_start(File) :-
logging(no, _),
!,
open(File, write, STR),
retractall(logging(_,_)),
assert(logging(File, STR)).

log_end :-
logging(no, _),
!.
log_end :-
logging(_File, STR),
close(STR),
fail.
log_end :-
retractall(logging(_,_)),
assert(logging(no, _)).

log_suspend(logging(File,STR)) :-
logging(File, STR),
retractall(logging(_,_)),
assert(logging(no, _)).

log_resume(logging(File,STR)) :-
retractall(logging(_,_)),
assert(logging(File, STR)).

logging(no, _),
!.
logging(_File, STR),
!,
write(STR, X),
write(STR, '.'),
nl(STR).
writex(X),
writex('.'),
nlx.

writex(X) :-
logging(no, _),
!,
write(X).
writex(X) :-
logging(_, STR),
write(X),
write(STR, X).

nlx :-
logging(no, _),
!,
nl.
nlx :-
logging(_, STR),
nl,
nl(STR).

tabx(X) :-
logging(no, _),
!,
tab(X).
tabx(X) :-
logging(_, STR),
tab(X),
tab(STR, X).

%%
%%  Batch
%%
batch :-
nl, write('# Start'), nl,
% prolog_flag(syntax_errors, _, quiet),
set_output_form(Output),
batch_prove(Sequent),
!,
flush_out,
halt.
batch :-
nl, write('# Syntax error'), nl,
flush_out,
halt.

batch_prove((X <--> Y)) :- !,
batch_prove((X --> Y)),
nl,
batch_prove((Y --> X)).
batch_prove(S0) :-
(
convert_to_seq(S0, S),
sequentq(S)
;
formulaq(S0),
S = ([] --> [S0])
),
!,
write('# Proving '), write(S), nl,
statistics(runtime, _),
(prove(S, P) ->
statistics(runtime, [_,T]),
nl,
write('# BEGIN Proof'), nl,
print_proof(P),
nl, write('# END Proof'), nl,
nl, write('# Proved in '),
write(T), write(' msec.'), nl
;
nl, write('# Fail to prove'), nl
).

%%
%%  Initialization
%%
:- seq_init.

Thanks ! I paste here leanseq.pl for the propositional case only. It contains a LaTeX printer that works, but I did not succeed to use it for the FOL case. Maybe it can help:

% -----------------------------------------------------------------
% leanseq.pl - A sequent calculus prover implemented in Prolog
% -----------------------------------------------------------------
:- use_module(library(lists)).
:- use_module(library(ordsets)).
:- use_module(library(time)).
:- use_module(library(terms)).
% :- [bussproofs].

% operator definitions (TPTP syntax)

:- op( 500, fy, ~).     % negation
:- op(1000, xfy, &).    % conjunction
:- op(1100, xfy, '|').  % disjunction
:- op(1110, xfy, =>).   % conditional
:- op(1120, xfy, <=>).  % biconditional
% :- op(500, fy, !).     % universal quantifier:  ![X]:
% :- op(500, fy, ?).     % existential quantifier:  ?[X]:
% :- op(500,xfy, :).

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

prove2(F,W):-
time(prove([]>[F],P)),
term_lower_upper(P,J),
nl,
write('Prolog output : '), write(P),
nl,
nl,
latex(J,W),!,
nl,
nl.

decide(F) :- prove2(F, _W).
% -----------------------------------------------------------------

%% 1. Initial rule: if G and D are strings [i.e. lists] of atomic formulae,
%% then G > D  is a theorem if some atomic formula occurs on both sides of the arrow:

prove(G>D, ax(G>D, ax)):-
list_to_ord_set(G,Ord_G),
list_to_ord_set(D,Ord_D),
\+ ord_disjoint(Ord_G,Ord_D),!.

/*
prove(G>D, ax(G>D, ax)):-
member(A,G),
member(B,D),
A==B,!.
*/
% In the ten rules listed below, G and D, are always
% strings (possibly empty) of atomic formulae.
% FIRST, NON-BRANCHING RULES
%% 2. Conditional on the  right
prove(G>D, rcond(G>D,P)):-
select((A=>B),D,D1),!,
prove([A|G]>[B|D1],P).
%% 3. Disjunction on the right
prove(G>D, ror(G>D, P)):-
select((A|B),D,D1),!,
prove(G>[A,B|D1],P).
%% 4. Negation on the right
prove(G>D, rneg(G>D,P)):-
select(~A,D,D1),!,
prove([A|G]>D1,P).
%% 5. Negation on the left
prove(G>D, lneg(G>D,P)):-
select(~A,G,G1),!,
prove(G1>[A|D],P).
%% 6. Conjunction on the left
prove(G>D, land(G>D,P)):-
select((A&B),G,G1),!,
prove([A,B|G1]>D,P).
% SECOND, BRANCHING RULES
%% 7. Biconditional on the right
prove(G>D, rbicond(G>D,P1,P2)):-
select((A<=>B),D,D1),!,
prove([A|G]>[B|D1],P1),
prove([B|G]>[A|D1], P2).
%% 8. Biconditional on the left
prove(G>D, lbicond(G>D, P1,P2)):-
select((A<=>B),G,G1),!,
prove([A,B|G1]>D,P1),
prove(G1>[A,B|D],P2).
%% 9. Conditional on the left
prove(G>D, lcond(G>D,P1,P2)):-
select((A=>B),G,G1),!,
prove(G1>[A|D],P1),
prove([B|G1]>D,P2).
%% 10. Conjunction on the right
prove(G>D, rand(G>D,P1,P2)):-
select((A&B),D,D1),!,
prove(G>[A|D1],P1),
prove(G>[B|D1],P2).
%% 11. Disjunction on the left
prove(G>D, lor(G>D, P1,P2)):-
select((A|B),G,G1),!,
prove([A|G1]>D, P1),
prove([B|G1]>D, P2).

% universal quantifier

% Third - One and only one refutation rule.
% NB: this rule in Prolog must be the last one in the order of clauses.
%% 12 - Failure-rule
prove(G>D, asq(G>D, asq)):-
ord_disjoint(G,D),!.

/*
Now, to upcase atomic variables in LaTeX output, the following code is Carlo Capelli's
https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/118
<https://swi-prolog.discourse.group/t/how-to-use-of-upcase-atom-2-to-get-uppercase-letters-in-an-output/4693/123?u=joseph-vidal-rosset
*/

term_lower_upper(Lower,Upper) :-
(   compound(Lower)
->  mapargs(term_lower_upper,Lower,Upper)
;   is_list(Lower)
->  maplist(term_lower_upper,Lower,Upper)
;   var(Lower)
->  Upper = Lower
;   atomic(Lower) % this should be useless
->  upcase_atom(Lower,Upper)
;   throw(term_lower_upper(Lower,Upper))
).

/******************************************************************/
/* Pretty Printing                                                */
/******************************************************************/

atom_split(X, D, L) :-
atomic_list_concat(L, D, X).

latex(H, J) :-
latex_root(H, J, L, []),
atom_split(Y, '', L),
write(Y),nl.

latex_root(P, J) --> ['\\begin{prooftree}'], latex_proof(P, J), ['\\end{prooftree}'].

latex_proof(ax(S,U), J) --> ['\\RightLabel{$Ax.$} \\AxiomC{} \\UnaryInfC{'],
latex_sequent(S, ax(S,U), J), ['}'].
latex_proof(rcond(S,P), J) --> latex_proof(P, J),
['\\RightLabel{$R\\to$} \\UnaryInfC{'],
latex_sequent(S, rcond(S,P), J), ['}'].
latex_proof(land(S,P), J) --> latex_proof(P, J),
['\\RightLabel{$L\\land$} \\UnaryInfC{'],
latex_sequent(S, land(S,P), J), ['}'].
latex_proof(ror(S,P), J) --> latex_proof(P, J),
['\\RightLabel{$R\\lor$} \\UnaryInfC{'],
latex_sequent(S, ror(S,P), J), ['}'].
latex_proof(lneg(S,P), J) --> latex_proof(P, J),
['\\RightLabel{$L\\neg$} \\UnaryInfC{'],
latex_sequent(S, lneg(S,P), J), ['}'].
latex_proof(rneg(S,P), J) --> latex_proof(P, J),
['\\RightLabel{$R\\neg$} \\UnaryInfC{'],
latex_sequent(S, rneg(S,P), J), ['}'].
latex_proof(rand(S,P,Q), J) --> latex_proof(P, J), latex_proof(Q, J),
['\\RightLabel{$R\\land$} \\BinaryInfC{'],
latex_sequent(S, rand(S,P,Q), J), ['}'].
latex_proof(lor(S,P,Q), J) --> latex_proof(P, J), latex_proof(Q, J),
['\\RightLabel{$L\\lor$} \\BinaryInfC{'],
latex_sequent(S, lor(S,P,Q), J), ['}'].
latex_proof(lcond(S,P,Q), J) --> latex_proof(P, J), latex_proof(Q, J),
['\\RightLabel{$L\\to$} \\BinaryInfC{'],
latex_sequent(S, lcond(S,P,Q), J), ['}'].
latex_proof(lbicond(S,P,Q), J) --> latex_proof(P, J), latex_proof(Q, J),
['\\RightLabel{$R\\leftrightarrow$} \\BinaryInfC{'],
latex_sequent(S, lbicond(S,P,Q), J), ['}'].
latex_proof(rbicond(S,P,Q), J) --> latex_proof(P, J), latex_proof(Q, J),
['\\RightLabel{$R\\leftrightarrow$} \\BinaryInfC{'],
latex_sequent(S, rbicond(S,P,Q), J), ['}'].
latex_proof(asq(S,U), J) --> ['\\RightLabel{$Asq.$} \\AxiomC{} \\UnaryInfC{'],
latex_antisequent(S, asq(S,U), J), ['}'].

latex_sequent(G > D, P, J) --> ['$'], latex_list(G, P, left, 0, J), [' \\vdash '], latex_list(D, P, right, 0, J), ['$'].

latex_antisequent(G > D, P, J) --> ['$'], latex_list(G, P, left, 0, J), [' \\nvdash '], latex_list(D, P, right, 0, J), ['$'].

latex_list([], _, _, _, _) --> [].
% latex_list([X|L], P, F, N, J) --> {has_usage(P, F, N)}, !, latex_formula(X, J), {M is N+1}, latex_rest(L, P, F, M, J).
latex_list([X|L], P, F, N, J) --> latex_formula(X, J), {M is N+1}, latex_rest(L, P, F, M, J).
latex_list([_|L], P, F, N, J) --> {M is N+1}, latex_list(L, P, F, M, J).

latex_rest([], _, _, _, _) --> [].
% latex_rest([X|L], P, F, N, J) --> {has_usage(P, F, N)}, !, [', '], latex_formula(X, J), {M is N+1}, latex_rest(L, P, F, M, J).
latex_rest([X|L], P, F, N, J) --> [', '], latex_formula(X, J), {M is N+1}, latex_rest(L, P, F, M, J).
latex_rest([_|L], P, F, N, J) --> {M is N+1}, latex_rest(L, P, F, M, J).

latex_formula(~A, J) --> !, ['\\neg '], latex_term(A, J).
latex_formula((A&B), J) --> !, latex_term(A, J), [' \\land '], latex_term(B, J).
latex_formula((A|B), J) --> !, latex_term(A, J), [' \\lor '], latex_term(B, J).
latex_formula((A=>B), J) --> !, latex_term(A, J), [' \\to '], latex_term(B, J).
latex_formula((A<=>B), J) --> !, latex_term(A, J), [' \\leftrightarrow '], latex_term(B, J).
% latex_formula(![X], J) --> !, ['\\forall '], latex_term(X, J).
% latex_formula(?[Y], J) --> !, ['\\exists '], latex_term(Y, J).
latex_formula(X, J) --> latex_factor(X, J).

latex_term(~A, J) --> !, ['\\neg '], latex_term(A, J).
latex_term((A&B), J) --> !, ['('], latex_term(A, J), [' \\land '], latex_term(B, J), [')'].
latex_term((A|B), J) --> !, ['('], latex_term(A, J), [' \\lor '], latex_term(B, J), [')'].
latex_term((A=>B), J) --> !, ['('], latex_term(A, J), [' \\to '], latex_term(B, J), [')'].
latex_term((A<=>B), J) --> !, ['('], latex_term(A, J), [' \\leftrightarrow '], latex_term(B, J), [')'].
% latex_term(![X], J) --> !, ['\\forall '], latex_term(X, J).
% latex_term(?[Y], J) --> !, ['\\exists '], latex_term(Y, J).
latex_term(X, J) --> latex_factor(X, J).

latex_factor(X, J) --> {var(X), member(W = N, J), W == X}, !, [N].
latex_factor(X, _) --> {var(X)}, !, ['?'].
latex_factor(X, J) --> {X=..[F,Y|L]}, !, [F, '('], latex_factor(Y, J), latex_args(L, J), [')'].
latex_factor(X, _) --> [X].

latex_args([], _) --> [].
latex_args([X|L], J) --> [','], latex_factor(X, J), latex_args(L, J).

/*

Example:

?- decide(p => p).
% 10 inferences, 0.000 CPU in 0.000 seconds (97% CPU, 321926 Lips)

Prolog output : rcond([]>[(p=>p)],ax([p]>[p],ax))

\begin{prooftree}\RightLabel{$Ax.$} \AxiomC{} \UnaryInfC{$P \vdash P$}\RightLabel{$R\to$} \UnaryInfC{$\vdash P \to P$}\end{prooftree}
true.

?- decide(p => q).
% 36 inferences, 0.000 CPU in 0.000 seconds (92% CPU, 675371 Lips)

Prolog output : rcond([]>[(p=>q)],asq([p]>[q],asq))

\begin{prooftree}\RightLabel{$Asq.$} \AxiomC{} \UnaryInfC{$P \nvdash Q$}\RightLabel{$R\to$} \UnaryInfC{$\vdash P \to Q$}\end{prooftree}
true.

*/

Once I write codes which parses proof trees given in plain text, then renders into pdf/svg via latex/divpdfmx[/pdf2svg] using Paulson’s prooftree.tex. Although it was a work of mine more than 20 years ago, the CGI version was recovered recently to work without changes on core of the Prolog codes. I neither remember well details of the codes nor am interested in revising version. However I think now, using the dot language (graphviz) joint with latex might fit my purpose and hope also for your current work and useful to displaying graph structure like proof tree. Please let me know if this comment would be relevant to your post and interested in more details. Now I feel getting interested into the dot version though I have no idea in details.

Without code to test thanks to a clear “howto”, it is difficult for me to give an opinion.

I should post after I am sure that dot allow graphics (jpeg/pdf/svg) as a label of node or edges, but it is just personal expectation for now. I have to check it.

EDIT
A quick search " graphviz svg for node" returns positive answers. I will take time later
for more details.

EDIT
There exists dot2tex, which might be what I meant as far as I have tested
a sample file in the github.

Yes. The quotation of what Wolfgang wrote must go on:

[…] We therefore run a separate algorithm to find smallest countermodels.

In outline, this works as follows.

We transform the formulas for which we want to find a model into clausal normal form,
which gives us literal “constraints” that we’re trying to satisfy.
For example, Fa ∧ Fb is split into two constraints, Fa and Fb; ∀x∃yRxy is turned into Rxf(x);
Fa ∨ Fb is turned into the disjunctive constraint [Fa, Fb].

What I have put in bold fonts is nothing else than Skolemization…

1. I never wrote that Skolemization is the only way to make a model finder in FOL.
2. I never wrote that Jens Otten’s prover was sufficient to do it.

The goal is not to display LK sequent calculus, but Leanseq i.e. Lean sequent calculus. Jens’ Otten explanations are given in these slides. LK (more precisely, a sequent calculus akin to LK) has been translated by Tamura. It provides for example the following sequent proof in LaTeX via proof.sty:

Now, I do not know if it is possible or impossible to translate the leanseq proof of this same sequent in bussproofs.sty, but via portray_clause/1 we get already a much more clear proof of it (thanks to Jan Wielemaker to have insisted on this point) :

decide((?[Y]: ![X]: f(X,Y)) => (![X]: ?[Y]: f(X,Y))).
iteration:1
iteration:2
% 451 inferences, 0.000 CPU in 0.000 seconds (100% CPU, 3396008 Lips)

Prolog proof: r_to([]>[(?[A]:![B]:f(B, A)=>![B]: ?[A]:f(B, A))],
r_forall([?[A]:![B]:f(B, A)]>[![B]: ?[A]:f(B, A)],
l_exists([?[A]:![B]:f(B, A)]>[?[C]:f(f_sk(1, []), C)],
r_exists([![D]:f(D, f_sk(2, []))]>[?[C]:f(f_sk(1, []), C)],
l_forall([![D]:f(D, f_sk(2, []))]>[f(f_sk(1, []), f_sk(2, [])), ?[C]:f(f_sk(1, []), C)],
ax([f(f_sk(1, []), f_sk(2, [])), ![D]:f(D, f_sk(2, []))]>[f(f_sk(1, []), f_sk(2, [])), ?[C]:f(f_sk(1, []), C)],
ax)))))).
true.

Note that the proof is different. It has been producted via the program below, a bit different from the first I pasted at the beginning of this discussion.

% ---------------------------------------------------------------------------------
% leanseq.pl - A sequent calculus prover for classical F.O.L. implemented in Prolog
% ---------------------------------------------------------------------------------
% :- [latex_pc].
% operator definitions (TPTP syntax)
:- op( 500, fy, ~).     % negation
:- op(1000, xfy, &).    % conjunction
:- op(1100, xfy, '|').  % disjunction
:- op(1110, xfy, =>).   % conditional
:- op(1120, xfy, <=>).  % biconditional
:- op( 500, fy, !).     % universal quantifier:  ![X]:
:- op( 500, fy, ?).     % existential quantifier:  ?[X]:
:- op( 500,xfy, :).

% -----------------------------------------------------------------
decide(F) :-
prove(F,P),nl,
write('Prolog proof: '),
portray_clause(P),!.

prove(F,I,P) :-
I < 5,
print(iteration:I), nl,
prove([] > [F],[],I,1,_,P).

prove(F,I,P) :-
I1 is I+1,
I < 5,
prove(F,I1,P).

prove(F,P) :-
time(prove(F,1,P)).

% -----------------------------------------------------------------
% THE LOGICAL RULES
% 1.The axiom
prove(G > D,_,_,J,J,Proof) :-
member(A,G),
A\=(_&_), A\=(_|_), A\=(_=>_),
A\=(~_), A\=(!_), A\=(?_),
member(B,D),
unify_with_occurs_check(A,B),
Proof = ax(G > D,ax).

% FIRST, NON-BRANCHING RULES %
%% 2. Conditional on the  right
prove(G > D,FV,I,J,K,Proof) :-
select(A=>B,D,D1), !,
prove([A|G] > [B|D1],FV,I,J,K,Rule_applied),
Proof = r_to(G > D, Rule_applied).
%% 3. Disjunction on the right
prove(G > D,FV,I,J,K,Proof) :-
select(A|B,D,D1), !,
prove(G > [A,B|D1],FV,I,J,K,Rule_applied),
Proof = r_lor(G > D, Rule_applied).
%% 4. Negation on the right
prove(G > D,FV,I,J,K,Proof) :-
select(~A,D,D1), !,
prove([A|G] > D1,FV,I,J,K,Rule_applied),
Proof = r_neg(G > D, Rule_applied).
%% 5. Negation on the left
prove(G > D,FV,I,J,K,Proof) :-
select(~A,G,G1), !,
prove(G1 > [A|D],FV,I,J,K,Rule_applied),
Proof = l_neg(G > D, Rule_applied).
%% 6. Conjunction on the left
prove(G > D,FV,I,J,K,Proof) :-
select(A&B,G,G1), !,
prove([A,B|G1] > D,FV,I,J,K,Rule_applied),
Proof = l_land(G > D, Rule_applied).
% SECOND, BRANCHING PROPOSITIONAL LOGIC RULES
% 7. Biconditional on the right
prove(G>D,FV,I,J,K,Proof) :-
select((A<=>B),D,D1),!,
prove([A|G]>[B|D1],FV,I,J,J1,Rule_applied1),
prove([B|G]>[A|D1],FV,I,J1,K,Rule_applied2),
Proof = l_leftrightarrow(G > D, Rule_applied1, Rule_applied2).
%% 8. Biconditional on the left
prove(G>D,FV,I,J,K,Proof):-
select((A<=>B),G,G1),!,
prove([A,B|G1]>D,FV,I,J,J1,Rule_applied1),
prove(G1>[A,B|D],FV,I,J1,K,Rule_applied2),
Proof = l_leftrightarrow(G > D, Rule_applied1, Rule_applied2).
%% 9. Conditional on the left
prove(G > D,FV,I,J,K,Proof) :-
select(A=>B,G,G1), !,
prove(G1 > [A|D],FV,I,J,J1,Rule_applied1),
prove([B|G1] > D,FV,I,J1,K,Rule_applied2),
Proof = l_to(G > D, Rule_applied1, Rule_applied2).
%% 10. Conjunction on the right
prove(G > D,FV,I,J,K,Proof) :-
select(A&B,D,D1), !,
prove(G > [A|D1],FV,I,J,J1,Rule_applied1),
prove(G > [B|D1],FV,I,J1,K,Rule_applied2),
Proof = r_land(G > D, Rule_applied1, Rule_applied2).
%% 11. Disjunction on the left
prove(G > D,FV,I,J,K,Proof) :-
select(A|B,G,G1), !,
prove([A|G1] > D,FV,I,J,J1,Rule_applied1),
prove([B|G1] > D,FV,I,J1,K,Rule_applied2),
Proof = l_lor(G > D, Rule_applied1, Rule_applied2).
%% QUANTIFICATION RULES
% 12. universal quantifier on the right
prove(G > D,FV,I,J,K,Proof) :-
select((![X]:A),D,D1),!,
copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
J1 is J+1,
prove(G > [A1|D1],FV,I,J1,K,Rule_applied),
Proof = r_forall(G > D, Rule_applied).
% 13. existential quantifier on the left
prove(G > D,FV,I,J,K,Proof) :-
select((?[X]:A),G,G1),!,
copy_term((X:A,FV),(f_sk(J,FV):A1,FV)),
J1 is J+1,
prove([A1|G1] > D,FV,I,J1,K,Rule_applied),
Proof = l_exists(G > D, Rule_applied).
% 14. existential quantifier on the right
prove(G > D,FV,I,J,K,Proof) :-
member((?[X]:A),D),
\+ length(FV,I),
copy_term((X:A,FV),(Y:A1,FV)),
prove(G > [A1|D],[Y|FV],I,J,K,Rule_applied),
Proof = r_exists(G > D, Rule_applied).
% 15. universal quantifier on the left
prove(G > D,FV,I,J,K,Proof) :-
member((![X]:A),G),
\+ length(FV,I),
copy_term((X:A,FV),(Y:A1,FV)),
prove([A1|G] > D,[Y|FV],I,J,K,Rule_applied),
Proof = l_forall(G > D, Rule_applied).

%% END of leanseq.pl code

There is an interesting comparison between Jens Otten’s Prover and Naoyuki Tamura’s. In his slides Jens Otten wrote:

And indeed, whith Jens’ prover, we get :

?- decide((![X]: f(a) => ![Y]: f(Y))).
iteration:1
iteration:2
iteration:3
iteration:4
% 26,717 inferences, 0.006 CPU in 0.006 seconds (100% CPU, 4486571 Lips)
false.

By contrast with Naoyuki’s prover:

Sequent Calculus Prover ver 2.0 in Prolog
by Naoyuki Tamura (tamura@kobe-u.ac.jp)
cl(first)> X@f(a) --> Y@f(Y).
_7964@f(a)-->_7970@f(_7970).
Trying to prove with threshold = 0
Succeed in proving a@f(a) --> a@f(a) (0 msec.)
pretty:1 =
----------------- Ax
a@f(a) --> a@f(a)
yes

And we can also compare the proofs for the valid sequent ∀x Fx → ∀y Fy . Leanseq by Jens Otten makes perfectly the job:

?- decide((![X]: f(X) => ![Y]: f(Y))).
iteration:1
% 90 inferences, 0.000 CPU in 0.000 seconds (97% CPU, 480179 Lips)

Prolog proof: r_to([]>[(![A]:f(A)=>![B]:f(B))],
r_forall([![A]:f(A)]>[![B]:f(B)],
l_forall([![A]:f(A)]>[f(f_sk(1, []))],
ax([f(f_sk(1, [])), ![A]:f(A)]>[f(f_sk(1, []))],
ax)))).
true.

By contrast, the output of seqprover.pl is not adequate:

cl(first)> X@f(X) --> Y@f(Y).
_7960@f(_7960)-->_7970@f(_7970).
Trying to prove with threshold = 0
Succeed in proving _7960@f(_7960) --> _7960@f(_7960) (0 msec.)
pretty:2 =
----------------- Ax
X@f(X) --> X@f(X)
yes
cl(first)>

I have a very simple question to help understand the pretty-printing. I get the following output:

decide(((a => b) => a => a)).
iteration:1
% 29 inferences, 0.000 CPU in 0.000 seconds (99% CPU, 300708 Lips)

Prolog Proof: r_to([]>[((a=>b)=>a=>a)],
r_to([(a=>b)]>[(a=>a)], ax([a, (a=>b)]>[a], ax))).

LaTeX Proof: \begin{prooftree}\RightLabel{$Ax.$} \AxiomC{} \UnaryInfC{$A, A \to B \vdash A$}\RightLabel{$R\to$} \UnaryInfC{$A \to B \vdash A \to A$}\RightLabel{$R\to$} \UnaryInfC{$\vdash (A \to B) \to (A \to A)$}\end{prooftree}

true.

It would be better to get:

LaTeX Proof:
\begin{prooftree}
\RightLabel{$Ax.$}
\AxiomC{} \UnaryInfC{$A, A \to B \vdash A$}
\RightLabel{$R\to$}
\UnaryInfC{$A \to B \vdash A \to A$}
\RightLabel{$R\to$}
\UnaryInfC{$\vdash (A \to B) \to (A \to A)$}
\end{prooftree}

The first new line can easily be obtained by the “driver” in leanseq.pl, but the others depend on the pretty-printing file that is with DCG, and I do not succeed to dot it, even if it is easy to see that after each
}
we need a new line…

?- decide((((a => b) => a) => a)).
iteration:1
% 61 inferences, 0.000 CPU in 0.004 seconds (2% CPU, 702360 Lips)

Prolog Proof: r_to([]>[(((a=>b)=>a)=>a)],
l_to([((a=>b)=>a)]>[a],
r_to([]>[(a=>b), a], ax([a]>[b, a], ax)),
ax([a]>[a], ax))).

LaTeX Proof:

\begin{prooftree}
\RightLabel{$Ax.$}
\AxiomC{}
\UnaryInfC{$A \vdash B, A$}
\RightLabel{$R\to$}
\UnaryInfC{$\vdash A \to B, A$}
\RightLabel{$Ax.$}
\AxiomC{}
\UnaryInfC{$A \vdash A$}
\RightLabel{$L\to$}
\BinaryInfC{$(A \to B) \to A \vdash A$}
\RightLabel{$R\to$}
\UnaryInfC{$\vdash ((A \to B) \to A) \to A$}
\end{prooftree}

true.

?-

Apart from this bug, Naoyuki’s prover has some interesting features, among which it provides LaTex output of FOL proofs. Therefore it would be possible to change the code of Leanseq prove, preserving its soundness but allowing LaTeX FOL proofs.

I believed that it was possible to use Naoyuki code only to replace the rules for quantification, in order to cancel FV,I,J,K in Jens Prover and to come back to a structure that is propositional calculus leanseq’s prover. But all my tentatives fail.

Ugliness is not really the problem, because what is ugly can become pretty. It is more difficult to obtain a correct first result. Thanks for your help !