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.

Your help is welcome.
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.

What are your rules of unprovability? FOL calculus doesn’t have such
rules, since the unprovable formulas are not recursively enumerable.

What you can nevertheless do, is for example try to find a finite counter model,
for example via mace4 by William McCune. You can even do Sudoku with it:

How Mace4 does Sudoku
https://www.cs.unm.edu/~mccune/sudoku/details.html

But what if the counter model is infinite?

Edit 25.04.2024
Instead of using mace4 write your own finite counter model finder in
Prolog, for example by a simple backtracking over finite models.

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, this is the tool by Wolfgang Schwarz it does a tableaux proof search
and a finite model search at the same time in the browser. I don’t know
exactly how he does it, but its open source.

About his finite model search he writes:

The Modelfinder
Often there are simple countermodels that are hard to find through
the tableau method. We therefore run a separate algorithm to find
smallest countermodels.
https://github.com/wo/tpg?tab=readme-ov-file#the-modelfinder

call_with_depth_limit/3 cannot do that. call_with_depth_limit/3 doesn’t
provide you a separate algorithm different from the calculus at hand.

Edit 25.04.2024
You can imagine a finite model finder as a Quine algorithm, whereas
a 1st order Quine algorithm takes a propositional variable P and assigns
it 0 or 1. A FOL Quine algorithm takes a predicate variable P of arity n.

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.

Lets say you don’t care about performance. You could proceed
as follows. Incrementally fix a domain size N, i.e. let it run through
0, 1, 2, 3, … thats the number of elements in the domain of the

models you are currently examining, whether one of them satisfies
a given first order formula F. First you have to get rid of the universal
and existential quantifiers in the first order formula F and turn it into a

zero order formula G. Use these transformation rules:

/* Validity in Domain D = {0, .., N-1} */
∃xA(x) ~~> A(0) v .. v A(N-1)
∀xA(x) ~~> A(0) & .. & A(N-1)

If F was a closed first order formula then G will be indeed a zero
order formula, if you identify each prime formula as a propositional
variable. Now you can apply a modified Quine algorithm to G,

that attacks the prime formulas of G.

Edit 27.04.2024
Lets make it a little advent of code. Who can implement this FOL
Quine Algorithm? And then solve this problem. Assume we have family
database and definitions for father, grand father etc…

“Im my own grandpa”

Show that the above sentence has a model, if the database
contains only definitions and no database constraints. Can
you find one such model with the FOL Quine Algorithm?

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 is what Wolfgang Schwarz uses. I do not propose a model
finder with anything Skolem functions. You must be mistaken.
Its much much more trivial, the domain expansion I propose.

Its literally just the definition of validity in a finite domain.
Also I put aside for the moment function symbols, there are
enough interesting FOL examples without function symbols

such as the Grandpa example. Again the expansion trivially reads:

Here are some example finite domain expansions, the
Drinker Paradox with N=1 and N=2:

?- expand(![X]:(d(X) => ?[Y]:d(Y)), 1, R).
R = (d(0)=>d(0)).

?- expand(![X]:(d(X) => ?[Y]:d(Y)), 2, R).
R = ((d(1)=>d(1)| d(0))&(d(0)=>d(1)| d(0))).

For a closed formula after expansion all prime formulas will be ground,
its a form of grounding. The modified Quine algorithm has now to
elaborate on prime formulas such as d(1) and d(0) to make them

true or false. And this is the code of the expansion that gets rid
of all first order quantifiers, it assumes that the bound variables
are separated away, i.e. distinct, and then uses copy_term/2:

% expand(+Formula, +Integer, -Formula)
expand((~ A), N, (~ X)) :- !, expand(A, N, X).
expand((A & B), N, (X & Y)) :- !, expand(A, N, X), expand(B, N, Y).
expand((A | B), N, (X | Y)) :- !, expand(A, N, X), expand(B, N, Y).
expand((A => B), N, (X => Y)) :- !, expand(A, N, X), expand(B, N, Y).
expand((A <=> B), N, (X <=> Y)) :- !, expand(A, N, X), expand(B, N, Y).
expand(![X]:A, N, R) :- copies(N, X, A, L), !, 
   expand_and(L, N, R).
expand(?[X]:A, N, R) :- copies(N, X, A, L), !, 
   expand_or(L, N, R).
expand(A, _, A).

% expand_and(+List, +Integer, -Formula)
expand_and([A], N, X) :- !, expand(A, N, X).
expand_and([A|L], N, (X & R)) :- expand(A, N, X), 
   expand_and(L, N, R).

% expand_or(+List, +Integer, -Formula)
expand_or([A], N, X) :- !, expand(A, N, X).
expand_or([A|L], N, (X | R)) :- expand(A, N, X), 
   expand_or(L, N, R).

% copies(+Integer, +Var, +Formula, -List)
copies(0, _, _, []).
copies(N, X, A, [B|L]) :- N > 0,
   M is N-1,
   copy_term(X-A, M-B),
   copies(M, X, A, L).

Grounding is silly technique that is often discussed in connection with ASP:

image
https://digitalcommons.unomaha.edu/cgi/viewcontent.cgi?article=3933&context=studentwork

But my goal here is to demonstrated a silly model finder based on Quine algorithm.
Ultimately I want to use the model finder to demonstrate that this is possible, given a
usual ontology for family terms, since they do not represent biological constraints:

On a side note it should be said grounding can be also used to deal with function
symbols. Although to stay silly I would not go in the direction of Herbrand domain,
rather use Fraïssé style relational modelling of functions. Thats also viable,

in case we want to include function symbols as well in the model finder.

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,
	  readx(STR, X),
	  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) :-
	open(File, read, STR),
	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)).

readx(STR, X) :-
	read(STR, X),
	echo_read(STR, X).

echo_read(user_input, _X) :-
	logging(no, _),
	!.
echo_read(user_input, X) :-
	logging(_File, STR),
	!,
	write(STR, X),
	write(STR, '.'),
	nl(STR).
echo_read(_, X) :-
	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),
	read(Output),
	read(Sequent),
	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.

You agreed that Wolgang Schwartz does it right prover and model finder,
now you fall back to Jens Otten prover only? Why this change of mind?
And why would I need to lookup where ground/1 is used in a prover only?

It is irrelevant. Since a model finder is a separate algorithm from a prover.
Separate means not only that it is a different Prolog query distinct from the
Prolog prover invocation, it also means that it is a Prolog algorithm distinct

from the Prolog prover. Just like William McCune has two distinct programs
mace4 and prover9, you need two distinct Prolog programs, namely a
prover and a model finder. Thats also why call_with_depth_limit/3 is

irrelevant for the model finder problem. I wrote this already, similary
Wolfgang Schwartz has also two distinct programs, and I made the words
separate algorithm bold. You need to understand the meaning of this!

call_with_depth_limit/3 cannot do that. call_with_depth_limit/3 doesn’t
provide you a separate algorithm different from the calculus at hand.
That it is a separate algorithm also means that Skolemization is not

necessarely the approach to find a model. You can try to introduce
Skolemization into the model finder, but some model finders don’t use
Skolemization. You might do a literature search about model finders, you

will find that there are some model finders without Skolemization at all!

Ok, the modified Quine algorithm wasn’t that difficult. Here is some
run with the expanded Drinker paradox. Since the Drinker paradox
is generaly valid, the modified Quine algorithm only finds models that

make it True. True and False are encoded as 1 and 0:

?- quine((d(0)=>d(0)), L, V).
L = [d(0)-0],
V = 1 ;
L = [d(0)-1],
V = 1.

?- quine(((d(1)=>d(1)| d(0))&(d(0)=>d(1)| d(0))), L, V).
L = [d(1)-0, d(0)-0],
V = 1 ;
L = [d(1)-0, d(0)-1],
V = 1 ;
L = [d(1)-1],
V = 1.

Now you have to combine the expansion that gets rid of the first order
quantifiers with the modified Quine algorithm, to go through model sizes
N = 1, 2, 3, etc.. and look for a model that values to False i.e. 0, and

there you got your simple FOL counter model finder, a program derived
from a program for propositional model finding, i.e. the Quine algorithm. No
Skolemization used neither in the expansion nor in the model search:

% eval(+Formula, -Formula)
eval((~ A), R) :- !, eval(A, X), simp(~ X, R).
eval((A & B), R) :- !, eval(A, X), eval(B, Y), simp((X & Y), R).
eval((A | B), R) :- !, eval(A, X), eval(B, Y), simp((X | Y), R).
eval((A => B), R) :- !, eval(A, X), eval(B, Y), simp((X => Y), R).
eval((A <=> B), R) :- !, eval(A, X), eval(B, Y), simp((X <=> Y), R).
eval(A, A).

% simp(+Formula, -Formula)
simp((~ 0), 1) :- !.
simp((~ 1), 0) :- !.
simp((0 & _), 0) :- !.
simp((_ & 0), 0) :- !.
simp((1 & A), A) :- !.
simp((A & 1), A) :- !.
simp((1 | _), 1) :- !.
simp((_ | 1), 1) :- !.
simp((0 | A), A) :- !.
simp((A | 0), A) :- !.
simp((1 => A), A) :- !.
simp((A => 0), R) :- !, simp((~ A), R).
simp((0 => _), 1) :- !.
simp((_ => 1), 1) :- !.
simp((1 <=> A), A) :- !.
simp((A <=> 1), A) :- !.
simp((0 <=> A), R) :- !, simp((~ A), R).
simp((A <=> 0), R) :- !, simp((~ A), R).
simp(A, A).

% candidate(+Formula, -Prime)
candidate(0, _) :- !, fail.
candidate(1, _) :- !, fail.
candidate((~ A), R) :- !, candidate(A, R).
candidate((A & _), R) :- candidate(A, R), !.
candidate((_ & B), R) :- !, candidate(B, R).
candidate((A | _), R) :- candidate(A, R), !.
candidate((_ | B), R) :- !, candidate(B, R).
candidate((A => _), R) :- candidate(A, R), !.
candidate((_ => B), R) :- !, candidate(B, R).
candidate((A <=> _), R) :- candidate(A, R), !.
candidate((_ <=> B), R) :- !, candidate(B, R).
candidate(A, A).

% subst(+Formula, +Prime, +Value, -Formula)
subst((~ A), K, V, (~ X)) :- !, subst(A, K, V, X).
subst((A & B), K, V, (X & Y)) :- !, subst(A, K, V, X), subst(B, K, V, Y).
subst((A | B), K, V, (X | Y)) :- !, subst(A, K, V, X), subst(B, K, V, Y).
subst((A => B), K, V, (X => Y)) :- !, subst(A, K, V, X), subst(B, K, V, Y).
subst((A <=> B), K, V, (X <=> Y)) :- !, subst(A, K, V, X), subst(B, K, V, Y).
subst(K, K, V, V) :- !.
subst(A, _, _, A).

% quine(+Formula, -Map, -Value)
quine(0, [], 0) :- !.
quine(1, [], 1) :- !.
quine(A, [K-V|R], W) :-
   candidate(A, K),
   subst(A, K, V, B), (V=0; V=1),
   eval(B, C), quine(C, R, W).

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.