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.
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).
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.
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 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.
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.
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…
I never wrote that Skolemization is the only way to make a model finder in FOL.
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) :
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
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…
Many thanks for your reply. Now the output is very nice:
?- 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 !
