prologlatexlogicswi-prologfirst-order-logic
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.
Whats exactly the problem?
I don’t find much problem for propositional logic:
:- show((p => p & ~ ~p)).
But for first order logic it is indeed ugly showing Ottens skolem expressions
and Ottens renaming of bound variables across a subformula:
/* Drinker Paradox */
:- show(![X]:(d(X) => ?[Y]:d(Y))).
A further refinement could be to include a term renderer that
replaces skolem expressions such as f_sk(1,[]) by constants
a, b, etc… as seen in Wolfgang Schwarz tableaux prover.
Source code so far:
https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/39
Edit 31.05.2024
After an additional rewrite/2 predicate and if you
don't mind using Unicode, but still some uglyness:
- Efficient solution for the same-fringe problem for binary trees
- Prolog: a person is a sibling of himself?
- When can I safely avoid storing temporary calculations in Prolog?
- gprolog: Getting a stacktrace after an exception
- Prolog - Solution of a riddle
- DCG LaTeX printer for FOL prover
- Is the structure of my Prolog expression isomorphic to the structure of the Liar Paradox?
- Syntax error: Operator expected in Prolog
- Assertion Failure in SWI-Prolog When Using pyswip to Consult a Prolog File
- Retract by partial match?
- Prolog - Applying predicate with one fixed arguments over list
- swi prolog game assignment . I want the player to unlock the door when the player has key but i can't seem to make the function work
- Logging interactive queries in SWI-Prolog
- Why does Prolog automatically backtrack in one case but not in another?
- maplist raises uncaught exception: error(existence_error(procedure,maplist/2),top_level/0)
- ECLiPSe create 2D matrix with C++ interfacing
- Prolog: Compress a list that contains segments of continuous numbers to a list which contains list of range of segments [start,end]
- How can i convert a list into a circular list in Prolog?
- uncaught exception: error(instantiation_error,(=<)/2)
- Early stop predicate with a `true` value in Prolog
- How to split list in Prolog?
- How to use Prolog from Java?
- Removing consecutive duplicates from a list in Prolog
- element/3 on matrix to find index returns range when value can only be at a single index
- Running SWI Prolog via Terminal Mac
- Prolog - How To Make Prolog Query Shorter?
- Prolog Filtering List using `findall` with in-line predicate or "lambda"
- What is the benefit of using SWI-Prolog's qsave_program to generate a binary?
- Why is Prolog's failure by negation not considered logical negation?
- check if object is a binary tree in prolog