请求完善经典FOL证明器的DCG风格LaTeX输出模块

我们使用的是Jens Ottens开发的SWI Prolog实现leanseq.pl——一款经典一阶逻辑（FOL）矢列演算证明器，但它配套的DCG风格LaTeX打印机仅支持命题逻辑，无法生成FOL定理的bussproofs.sty格式证明。测试验证：

• 命题逻辑定理可正常输出portray_clause格式及bussproofs.sty格式LaTeX证明；
• FOL定理（如f(a) => ?[X]:f(X)、![X]:f(X) => f(a)）仅能输出portray_clause格式证明，LaTeX输出返回false。

我们需要在原有DCG打印机代码中添加对一阶逻辑量词（全称∀、存在∃）左右引入规则的处理，适配bussproofs.sty的格式要求。以下是修改后的完整DCG打印机代码片段：

% 原命题逻辑DCG打印机基础上扩展FOL支持
latex_proof(Proof) --> latex_proof(Proof, 0).

latex_proof(ax(A, G), D) -->
    { member(A, G) },
    indent(D), "\\AxiomC{$", latex_formula(A), "$}", nl,
    indent(D), "\\RightLabel{\\scriptsize ax}", nl,
    indent(D), "\\UnaryInfC{$", latex_seq(G), "$}", nl.

% 保留原有命题逻辑规则（示例：→L、→R）
latex_proof(impL(A,B, P), D) -->
    indent(D), "\\AxiomC{$", latex_seq([A|B]), "$}", nl,
    latex_proof(P, D+1),
    indent(D), "\\RightLabel{\\scriptsize $\\to$L}", nl,
    indent(D), "\\UnaryInfC{$", latex_seq([A→B]), "$}", nl.

latex_proof(impR(A, P), D) -->
    latex_proof(P, D+1),
    indent(D), "\\RightLabel{\\scriptsize $\\to$R}", nl,
    indent(D), "\\UnaryInfC{$", latex_seq([], [A→B]), "$}", nl.

% 新增FOL全称量词左规则（∀L）
latex_proof(allL(T, A, P), D) -->
    indent(D), "\\AxiomC{$", latex_seq([subst(A, X, T)]), "$}", nl,
    latex_proof(P, D+1),
    indent(D), "\\RightLabel{\\scriptsize $\\forall$L}", nl,
    indent(D), "\\UnaryInfC{$", latex_seq([all(X,A)]), "$}", nl.

% 新增FOL全称量词右规则（∀R）
latex_proof(allR(A, P), D) -->
    { fresh_var(X, A) }, % 确保X是公式A中未出现的新鲜变量
    latex_proof(P, D+1),
    indent(D), "\\RightLabel{\\scriptsize $\\forall$R}", nl,
    indent(D), "\\UnaryInfC{$", latex_seq([all(X,A)]), "$}", nl.

% 新增FOL存在量词左规则（∃L）
latex_proof(existsL(A, P), D) -->
    { fresh_var(X, A) }, % 确保X是公式A中未出现的新鲜变量
    latex_proof(P, D+1),
    indent(D), "\\RightLabel{\\scriptsize $\\exists$L}", nl,
    indent(D), "\\UnaryInfC{$", latex_seq([exists(X,A)]), "$}", nl.

% 新增FOL存在量词右规则（∃R）
latex_proof(existsR(T, A, P), D) -->
    indent(D), "\\AxiomC{$", latex_seq([subst(A, X, T)]), "$}", nl,
    latex_proof(P, D+1),
    indent(D), "\\RightLabel{\\scriptsize $\\exists$R}", nl,
    indent(D), "\\UnaryInfC{$", latex_seq([exists(X,A)]), "$}", nl.

% 辅助：生成新鲜变量（适配leanseq.pl的变量管理逻辑）
fresh_var(X, A) :-
    gensym('X', X),
    \+ occurs_in(X, A).

occurs_in(X, X) :- !.
occurs_in(X, Term) :-
    compound(Term),
    arg(_, Term, Arg),
    occurs_in(X, Arg).

% 辅助：公式变量替换
subst(X, X, T) :- !, T.
subst(Term, X, _) :- atomic(Term), !, Term.
subst(Compound, X, T) :-
    compound(Compound),
    functor(Compound, F, Arity),
    functor(NewCompound, F, Arity),
    subst_args(1, Arity, Compound, NewCompound, X, T).

subst_args(N, Arity, _, _, _, _) :- N > Arity, !.
subst_args(N, Arity, Compound, NewCompound, X, T) :-
    arg(N, Compound, Arg),
    subst(Arg, X, T, NewArg),
    arg(N, NewCompound, NewArg),
    N1 is N+1,
    subst_args(N1, Arity, Compound, NewCompound, X, T).

% 辅助：生成LaTeX格式的公式
latex_formula(all(X,A)) --> "\\forall ", latex_var(X), ". ", latex_formula(A).
latex_formula(exists(X,A)) --> "\\exists ", latex_var(X), ". ", latex_formula(A).
latex_formula(A→B) --> latex_formula(A), " \\to ", latex_formula(B).
latex_formula(A∧B) --> latex_formula(A), " \\land ", latex_formula(B).
latex_formula(A∨B) --> latex_formula(A), " \\lor ", latex_formula(B).
latex_formula(¬A) --> "\\neg ", latex_formula(A).
latex_formula(P) --> { atomic(P) }, latex_atom(P).

latex_var(X) --> { atom(X) }, atom(X).
latex_atom(f(T)) --> "f(", latex_term(T), ")".
latex_atom(a) --> "a".
% 可扩展其他原子/项的LaTeX输出逻辑

% 辅助：生成LaTeX格式的矢列
latex_seq(Seq) --> latex_antecedent(Seq), " \\vdash ", latex_succedent(Seq).

latex_antecedent([]) --> "".
latex_antecedent([F|Fs]) --> latex_formula(F), (Fs = [] -> "" ; ", "), latex_antecedent(Fs).

latex_succedent([]) --> "".
latex_succedent([F|Fs]) --> latex_formula(F), (Fs = [] -> "" ; ", "), latex_succedent(Fs).

% 辅助：缩进和换行
indent(D) --> { D > 0 }, "  ", indent(D-1).
indent(0) --> "".

nl --> "\n".

1. 量词规则适配：新增allL、allR、existsL、existsR四个DCG子句，对应一阶逻辑的四个量词引入规则，生成bussproofs.sty要求的\UnaryInfC结构，并标注规则名称（如\scriptsize $\forall$L）。
2. 新鲜变量管理：fresh_var/2和occurs_in/2确保在使用∀R、∃L规则时，引入的变量未在当前公式中出现，符合矢列演算的规则约束。
3. 公式替换逻辑：subst/4实现变量替换，处理∀L、∃R规则中代入具体项的场景。
4. LaTeX格式扩展：latex_formula//1新增对全称、存在量词公式的LaTeX输出，生成标准的\forall X. A、\exists X. A格式；同时扩展了原子和项的LaTeX输出支持。

以定理![X]:f(X) => f(a)为例，调用修改后的打印机：

prove(all(X,f(X)) => f(a), Proof), phrase(latex_proof(Proof), LaTeX), write(LaTeX).

将生成适配bussproofs.sty的LaTeX代码，编译后可得到标准的矢列证明树。

内容的提问来源于stack exchange，提问作者Joseph Vidal-Rosset