用于 FOL 证明的 DCG LaTeX 打印机

问题描述 投票：0回答：1

以下SWI Prolog代码主要是Jens Ottens的leanseq.pl证明者用于经典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       %

及其 DCG 表示法的打印机，仅适用于命题逻辑的情况：


:- 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].

我没有成功完成这台打印机以获得经典一阶逻辑定理的 LaTeX (bussproofs.sty) 证明。如果有人成功打点并分享完成打印机的代码，我会很高兴。

最小示例：证明者和打印机在同一目录中，查阅证明者，可以看到，除了复杂性问题，经典命题逻辑的任何定理都是可证明的，并且输出都是通过描绘_子句给出的/1 并采用bussproofs.sty LaTeX 格式：

?- 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.

与一阶谓词演算的任何定理相比：

?- 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.

我不知道是否有可能完成打印机文件，以便在这个证明者的情况下为任何经典的 FOL 定理提供 LaTeX 证明，但这具有挑战性。

prolog latex logic swi-prolog first-order-logic
1个回答
0
投票

渲染时原始乳胶是什么样子。
到底是什么问题？

我没有发现命题逻辑有太多问题：

:- show((p => p & ~ ~p)).

enter image description here

但是一阶逻辑显示 Ottens skolem 函数确实很难看：

/* Drinker Paradox */
:- show(![X]:(d(X) => ?[Y]:d(Y))).

enter image description here

到目前为止的源代码：
https://swi-prolog.discourse.group/t/needing-help-with-call-with-depth-limit-3/7398/39

最新问题
© www.soinside.com 2019 - 2025. All rights reserved.