如何简洁地排版命题证明树？

Question

[更新为 CTAN 上的最新版本。请注意，大多数图像都是用早期代码创建的，间距有点压缩。当前间距显示在说明在论证中使用交叉引用的图像中。这是因为现在在树打包时可以正确考虑闭包符号。]

我会用防护树。毋庸置疑，我有偏见。另一方面，如果我能找到一个能完成我想要的工作的包，我很乐意不写这个包。

该软件包基于森林。

包装是森林。你可以像这样设置树：

...
\usepackage{prooftrees}
...
\begin{prooftree}
  {
    <preamble, if any>
  }
  <tree specification in forest's bracket notation>
\end{prooftree}
...

前言可以为空，但参数是必需的。也就是说，你可以有

\begin{prooftree}{}
  <tree>
\end{prooftree}

但不是

\begin{prooftree}
  <tree>
\end{prooftree}

默认情况下，当没有分支时，线条在左侧编号，级别分组。就树而言，这意味着当只有一个子级时，不会绘制指向父级的线条。

树中还有一些其他样式：

checked

将前提或子结论标记为已完成。默认情况下，使用勾号，但可以根据需要进行自定义。

close

关闭分支。默认情况下\otimes使用，但可以自定义。

这意味着你可以说

\documentclass[tikz,border=10pt]{standalone}
\usepackage{prooftrees}% version 0.09
\begin{document}
\begin{prooftree}
  {
    close with={\ensuremath{\ast}}
  }
  [P \land (Q \lor \lnot R), checked
    [\lnot ((P \land Q) \land S), checked
      [\lnot (P \land S) \lor R, checked
        [\lnot\lnot S
          [P
            [Q \lor \lnot R, checked
              [\lnot (P \land Q), checked
                [\lnot P, close]
                [\lnot Q
                  [Q, close]
                  [\lnot R
                    [\lnot (P \land S), checked
                      [\lnot P, close]
                      [\lnot S, close]
                    ]
                    [R, close]
                  ]
                ]
              ]
              [\lnot S, close]
            ]
          ]
        ]
      ]
    ]
  ]
\end{prooftree}
\end{document}

生产

要将行号放在括号中并删除点，只需执行

\renewcommand*\linenumberstyle[1]{(#1)}

在画树之前

可以使用以下方式添加推论依据

just=<content>

例如

\renewcommand*\linenumberstyle[1]{(#1)}
\begin{prooftree}
  {
    close with={\ensuremath{\ast}},
  }
  [P \land (Q \lor \lnot R), checked
    [\lnot ((P \land Q) \land S), checked
      [\lnot (P \land S) \lor R, checked
        [\lnot\lnot S
          [P, just=from 1
            [Q \lor \lnot R, checked, just=from 1
              [\lnot (P \land Q), checked, just=from 2
                [\lnot P, close, just=from 7]
                [\lnot Q
                  [Q, close]
                  [\lnot R, just=from 6
                    [\lnot (P \land S), checked, just=from 3
                      [\lnot P, close, just=from 10]
                      [\lnot S, close]
                    ]
                    [R, close]
                  ]
                ]
              ]
              [\lnot S, close]
            ]
          ]
        ]
      ]
    ]
  ]
\end{prooftree}

这些在右侧对齐，因为行号在左侧对齐。

:在的参数中，还支持交叉引用just。默认情况下，这些设置在对齐的左侧（用于规则名称），但可以按如下方式切换。引用可以使用name节点的或相对节点名称。例如：

\documentclass[tikz,multi,border=10pt]{standalone}
\usepackage{prooftrees,amsmath}
\begin{document}
\renewcommand*\linenumberstyle[1]{(#1)}
\begin{prooftree}
  {
    close with={\ensuremath{\ast}},
    just refs right
  }
  [P \land (Q \lor \lnot R), checked
    [\lnot ((P \land Q) \land S), checked
      [\lnot (P \land S) \lor R, checked
        [\lnot\lnot S
          [P, just=from:!r1
            [Q \lor \lnot R, checked, just=from:!r1, name=bert
              [\lnot (P \land Q), checked, just=from:!r11
                [\lnot P, close, just=from:!u]
                [\lnot Q
                  [Q, close]
                  [\lnot R, just=from:bert
                    [\lnot (P \land S), checked, just=from:!r111
                      [\lnot P, close, just=from:!u]
                      [\lnot S, close]
                    ]
                    [R, close]
                  ]
                ]
              ]
              [\lnot S, close]
            ]
          ]
        ]
      ]
    ]
  ]
\end{prooftree}
\end{document}

生产

如果需要的话，同一系统支持引用close。

to prove=<contents>

可用于序言中，提供待证明的蕴涵或定理的陈述。例如

\begin{prooftree}
  {
    close with={\ensuremath{\ast}},
    to prove={ \{P \land (Q \lor \lnot R), \lnot ((P \land Q) \land S), \lnot (P \land S) \lor R \} \sststile{L}{} \lnot S }
  }
...

生产

也可以将行移动到后面的级别，无论是否进行解释。您的示例似乎不需要这些功能，因此它们与此无关。

Answer 1