DCG LaTeX printer for FOL prover
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) -->
['\\AxiomC{}\n \\RightLabel{$Ax.$}\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.
Minimal examples: the prover and the printer in the same directory, consult the prover, and see that, except complexity issue, any theorem of classical propositional logic is provable, and that the output is both is given both via portray_clause/1 and in bussproofs.sty LaTeX format :
?- decide(~ ~ p => p).
% 46 inferences, 0.000 CPU in 0.000 seconds (97% CPU, 2196543 Lips)
P_Proof: r_to([]>[(~ ~p=>p)],
l_neg([~ ~p]>[p], r_neg([]>[~p, p], ax([p]>[p], ax)))).
L_Proof:
\begin{prooftree}
\AxiomC{}
\RightLabel{$Ax.$}
\UnaryInfC{$P \vdash P$}
\RightLabel{$R\neg$}
\UnaryInfC{$ \vdash \neg P , P$}
\RightLabel{$L\neg$}
\UnaryInfC{$\neg \neg P \vdash P$}
\RightLabel{$R\to$}
\UnaryInfC{$ \vdash \neg \neg P \to P$}
\end{prooftree}
true.
By contrast with any theorem of first order predicate calculus:
?- decide(f(a) => ?[X]: f(X)).
% 59 inferences, 0.000 CPU in 0.000 seconds (94% CPU, 701396 Lips)
P_Proof: r_to([]>[(f(a)=> ?[A]:f(A))],
r_exists([f(a)]>[?[A]:f(A)],
ax([f(a)]>[f(a), ?[A]:f(A)], ax))).
L_Proof:
false.
?- decide(![X]:f(X) => f(a)).
% 57 inferences, 0.000 CPU in 0.000 seconds (94% CPU, 680142 Lips)
P_Proof: r_to([]>[(![A]:f(A)=>f(a))],
l_forall([![A]:f(A)]>[f(a)],
ax([f(a), ![A]:f(A)]>[f(a)], ax))).
L_Proof:
false.
I do not know if it is possible to complete the printer file in order to provide LaTeX proofs for any classical FOL theorem in the case of this prover, but it is challenging.
Solution
How does your raw Latex look like when you
render it. What is exactly the problem?
I don’t find much problem for propositional logic,
basically using the Curry Howard isomorphism:
:- show((p => p & ~ ~p)).
- Unexpected Behavior in Prolog Water Sort Puzzle Solver: Duplicate Results, Persistent State, and GoalCheck Inconsistencies
- Prolog Binary Addition Issue?
- Prolog Design Pattern to extend module predicates
- What's the SLD tree for this query?
- Tron lightcycles AI in Prolog
- Verify_attributes in SICStus Prolog
- Extensional DCG Test Cases
- Prefix Parsing using Prolog
- Prolog: Difference between overriding predicate and using it
- Uneven tabling performance in BProlog 8.1
- Remove leading s(s(0)) in list
- Display the execution times for each goal of a predicate clause
- User input in prolog
- PROLOG with lambda expressions
- Best way to generate integer numbers in Prolog
- Grammar involving braces
- Remove leading zeros in list in Prolog
- Android and Prolog
- Attributed variables: library interfaces / implementations / portability
- Prolog - Palindrome Functor
- Is there a program that can draw a search tree of Prolog queries?
- How to use Prolog from Java?
- Command line argument vectors in Prolog?
- Does Prolog have a condition and restart system like Common Lisp?
- SWI Prolog - explanation on a solution
- Prolog DCG in infinite loop without a direct left recursion
- How to identify valid bodies and convertible terms
- Turbo Prolog: Create a palindrome by adding the smallest number of characters to the list
- Prolog order of clause body gives different results when using negation
- Problem With a Predicate to Check if X Occurs Exactly Four Times in a List