The following SWI Prolog code is mainly Jens Ottens’ leanseq.pl prover for classical FOL:
% ---------------------------------------------------------------------------------
% leanseq.pl - A sequent calculus prover for classical F.O.L. implemented in Prolog
% ---------------------------------------------------------------------------------
:- use_module(library(clpfd)).
:- use_module(library(lists)).
% :- use_module(library(ordsets)).
:- use_module(library(time)).
:- use_module(library(terms)).
:- [latex_prop].
% :- [latex_pred].
% ---------------------------------------------------------------------------------
% 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, :).
*/
% The driver -------------------------------------------------------
decide(Formula) :-
prove(Formula).
prove(Formula,I,Proof) :-
I < 10,
% print(iteration:I), nl,
prove([] > [Formula],[],I,1,_,Proof).
prove(Formula,I,Proof) :-
I1 is I+1,
I < 10,
prove(Formula,I1,Proof).
prove(Formula) :-
time(prove(Formula,1,Proof)),nl,
write('P_Proof: '),
portray_clause(Proof),!,
nl,
% buss_tex_print(Proof).
term_lower_upper(Proof,J),
nl,
write('L_Proof: '),nl,nl,
latex(J,_LaTeX_output),!,
nl,
nl.
% -----------------------------------------------------------------
% 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. 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).
%% 5. 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).
%% 6. 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).
% SECOND, BRANCHING PROPOSITIONAL LOGIC RULES %
%% 7. 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).
%% 8. 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).
%% 9. 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).
% 10. 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).
%% 11. 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).
%% 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 %
and its printer in DCGs notation, that works only for the case of propositional logic:
:- 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, :).
/*
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) % Check if Lower is an atomic term
-> upcase_atom(Lower, Upper) % Capitalize atoms for propositional calculus
; throw(term_lower_upper(Lower, Upper))
).
/******************************************************************/
/* Pretty Printing for propostional calculus */
/******************************************************************/
atom_split('', _, []) :- !. % Handle empty string case and cut to prevent backtracking
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}n'],
latex_proof(P, J),
['\end{prooftree}n'].
latex_proof(ax(S,U), J) -->
['\RightLabel{$Ax.$}n \AxiomC{}n \UnaryInfC{$'],
latex_sequent(S, ax(S,U), J),
['$}n'].
latex_proof(r_to(S,P), J) -->
latex_proof(P, J),
['\RightLabel{$R\to$}n \UnaryInfC{$'],
latex_sequent(S, r_to(S,P), J),
['$}n'].
latex_proof(l_land(S,P), J) -->
latex_proof(P, J),
['\RightLabel{$L\land$}n \UnaryInfC{$'],
latex_sequent(S, l_land(S,P), J),
['$}n'].
latex_proof(r_lor(S,P), J) -->
latex_proof(P, J),
['\RightLabel{$R\lor$}n \UnaryInfC{$'],
latex_sequent(S, r_lor(S,P), J),
['$}n'].
latex_proof(l_neg(S,P), J) -->
latex_proof(P, J),
['\RightLabel{$L\neg$}n \UnaryInfC{$'],
latex_sequent(S, l_neg(S,P), J),
['$}n'].
latex_proof(r_neg(S,P), J) -->
latex_proof(P, J),
['\RightLabel{$R\neg$}n \UnaryInfC{$'],
latex_sequent(S, r_neg(S,P), J),
['$}n'].
latex_proof(r_land(S,P,Q), J) -->
latex_proof(P, J),
latex_proof(Q, J),
['\RightLabel{$R\land$}n \BinaryInfC{$'],
latex_sequent(S, r_land(S,P,Q), J),
['$}n'].
latex_proof(l_lor(S,P,Q), J) -->
latex_proof(P, J),
latex_proof(Q, J),
['\RightLabel{$L\lor$}n \BinaryInfC{$'],
latex_sequent(S, l_lor(S,P,Q), J),
['$}n'].
latex_proof(l_to(S,P,Q), J) -->
latex_proof(P, J),
latex_proof(Q, J),
['\RightLabel{$L\to$}n \BinaryInfC{$'],
latex_sequent(S, l_to(S,P,Q), J),
['$}n'].
latex_proof(l_leftrightarrow(S,P,Q), J) -->
latex_proof(P, J),
latex_proof(Q, J),
['\RightLabel{$R\leftrightarrow$}n \BinaryInfC{$'],
latex_sequent(S, l_leftrightarrowd(S,P,Q), J),
['$}n'].
latex_proof(r_leftrightarrow(S,P,Q), J) -->
latex_proof(P, J),
latex_proof(Q, J),
['\RightLabel{$R\leftrightarrow$}n \BinaryInfC{$'],
latex_sequent(S, r_leftrightarrow(S,P,Q), J),
['$}n'].
latex_sequent(G > D, _, J) -->
latex_list(G, 0, J),
[' \vdash '],
latex_list(D, 0, J).
latex_list([X|L], N, J) -->
latex_formula(X, J),
{M is N+1},
latex_rest(L, M, J).
latex_list([_|L], N, J) -->
{M is N+1},
latex_list(L, M, J).
latex_list([], _,_) -->
[].
latex_rest([X|L], N, J) -->
[' , '],
latex_formula(X, J),
{M is N+1},
latex_rest(L, M, J).
latex_rest([_|L], N, J) -->
{M is N+1},
latex_rest(L, M, J).
latex_rest([], _, _) -->
[].
latex_formula(~A, J) -->
!,
['\neg '],
latex_formula(A, J).
latex_formula((A&B), J) -->
!,
latex_formula(A, J),
[' \land '],
latex_formula(B, J).
latex_formula((A|B), J) -->
!,
latex_formula(A, J),
[' \lor '],
latex_formula(B, J).
latex_formula((A=>B), J) -->
!,
latex_formula(A, J),
[' \to '],
latex_formula(B, J).
latex_formula((A<=>B), J) -->
!,
latex_formula(A, J),
[' \leftrightarrow '],
latex_formula(B, J).
latex_formula(X, J) -->
latex_factor(X, J).
latex_factor(X, _) -->
[X].
I do not succeed to complete this printer to get LaTeX (bussproofs.sty) proofs for theorems of classical first order logic. I would be glad if someone would succeed to dot it and would share the code to complete the printer. Thanks.