☰

用于排版校样树的最佳软件包是什么？

tag-icon • tag-icon packages logic
用于排版校样树的最佳软件包是什么？

所以，我想排版一些证明树即推理规则树，类似自然演绎中的规则树（见下图）。您发现哪些最佳软件包可以实现此目的？它们具有哪些功能？

替代文本

答案1

Peter Smith 非常有用逻辑学家的 LaTeX页面提供了以下建议防下枝树以及自然演绎证明既有 Gentzen 序列风格（您似乎追求的是树状风格），也有 Fitch 风格。

我没有使用任何证明树的替代方案，因为我使用的是 Fitch 风格的自然演绎证明。但是，我发现 Smith 是最可靠的指南，并且他推荐了最好的证明树。山姆·巴斯的bussproofs.sty。史密斯还谈到了其他一些您可能想要了解的替代方案。

生成示例树的一个简单示例是：

\documentclass{article}
\usepackage{bussproofs}
\begin{document}
\begin{prooftree}
\AxiomC{A}
\UnaryInfC{B}
\AxiomC{C}
\BinaryInfC{D}
\AxiomC{E}
\AxiomC{F}
\BinaryInfC{G}
\UnaryInfC{H}
\BinaryInfC{J}
\end{prooftree}
\end{document}

答案2

我喜欢mathpartir（作者：Didier Remy）因其简单灵活的设计和智能布局概念而出名。该名称代表“段落模式中的数学公式”和“排版推理规则”。您可以使用它来排版许多规则定义。例如：

\begin{mathpar}
\inferrule[Foo]{A \\ B \\\\ C}{D}
\and
\inferrule[Bar]{X}{Y}
\end{mathpar}

规则

您还可以排版派生树：

\[
\inferrule* [left=Total]
  {\inferrule* [Left=Foo] {\inferrule* [Right=Bar,
                              leftskip=2em,rightskip=2em,vdots=1.5em]
      {a \\ a \\\\ bb \\ cc \\ dd}
      {ee}
    \\ ff \\ gg}
    {hh}
    \\
    \inferrule* [lab=XX]{uu \\ vv}{ww}}
    {(1)}
\]

替代文本

答案3

大部头书，埃布洛夫绝对是可行的方法。

正如该包的作者所写，

该结构很大程度上受到 bussproofs 包的启发，尤其是后缀表示法。我实际上编写了 ebproof，因为 bussproofs 中存在一些我不知道如何消除的限制，也因为我不喜欢该包中的一些选择（也因为编写它很有趣）。

以下代码：

\documentclass[border=10pt]{standalone}
\usepackage{ebproof}
\begin{document}
    \begin{prooftree}
        \hypo{A}
        \infer1{B}
        \hypo{C}
        \infer2{D}
        \hypo{E}
        \hypo{F}
        \infer2{G}
        \infer1{H}
        \infer2{J}
    \end{prooftree}
\end{document}

生成：

在此处输入图片描述

但是该软件包允许对样式、对齐、标签等进行许多细微的修改，使其成为我所知道的最模块化的选项。

答案4

简短补充：对于那些喜欢使用 bussproofs 生成输出，但又不愿意使用基于堆栈的语法的人，我编写了一个总线防护前端允许使用类似 Lisp 的简单语法来指定证明。在此语法中，您可以定义自定义运算符，包括优先级信息（这样该工具也可以处理括号的添加）。证明是从根开始指定的，这对某些人来说可能更直观；但它们仍然以通常的从叶到根的方式呈现。

输入示例：

(macro implies 0 "\Longrightarrow")
(defop neg "\neg " 40 prefix)
(defop modality "\left[#1\right]#2" 40 param)
(defop land " \land " 30 infix)
(defop text "\textrm{#1}" 99999 param)
(defop list ", " 10 infix)
(defop lor " \lor " 20 infix)
(defop seq "\implies  " 0 infix)

(proof (
    (lor  "asdf" (lor  "asdf" (neg  "asdf")))
    (seq  "" (modality  "p" "\phi"))
    (neg  (lor  "p" "q"))
    (land  (lor  "p" "q") (lor  "q" "p"))
    (lor  (land  "p" "q") (land  "q" "p"))
    (lor  "asdf" (lor  "asdf" "asdf")) <- "That's ``a'' right label!"
    "FancySplitRule 1" -> (seq  "" (list  (neg  "p") (neg  "q") (lor  "p" "q")))
    (
        "subtree1"
        "test"
        (
            "test"
            (seq  (lor  "p" (neg  "q")) "succedent")
            (neg  "p")
        )
    )
    (
        "subtree2"
        "test"
    )
    (
        (text  "And a third branch!!!")
    )
))

将被渲染为：

例如，使用下面的一行代码（对于 fish shell）：

java -jar ProofRenderer.jar -f $argv[1].pt -r standalone-latex -o $argv[1].tex -a "--fit-to-page" ; and pdflatex -interaction=batchmode $argv[1].tex

优点是抽象程度可变（您可以在字符串中使用纯 LaTeX，并且仅通过 Lisp 括号定义结构，或者您可以定义许多宏和操作，并且只使用类似 Lisp 的元素来构建树）、仍像往常一样渲染的从根到叶的符号以及对不同渲染器的可扩展性。缺点是您还需要另一个工具，并且不能直接将其包含在源代码中。请随意尝试 ;)

相关内容