Prooftrees 逻辑树序言示例

Question

以下示例不在文档中prooftrees（我认为需要更新版本的 TeX Live 才能使用该软件包）。问题是文档的.tex文件有一个巨大的序言。我需要一个最小的序言示例来运行该代码，这样我就可以开始尝试使用该软件包：

\begin{codcoeden}*[label=ptdefaults]{\pkg{prooftrees}: default settings}
\begin{prooftree}
{
to prove={\{P \vee (Q \vee \lnot R), P \lif \lnot R, Q \lif \lnot R\} \sststile{}{} \lnot R}
}
[P \vee (Q \vee \lnot R),  just=Ass, checked
[P \lif \lnot R,  just=Ass, checked
  [Q \lif \lnot R,  just=Ass, checked, name=last premise
    [\lnot\lnot R, just={$\lnot$ Conc}, name=not conc
      [P,  just={$\vee$ Elim:!uuuu}
        [\lnot P, close={:!u,!c}]
        [\lnot R,  close={:not conc,!c}, just={$\lif$ Elim:!uuuu}]]
      [Q \vee \lnot R
        [Q, move by=1
          [\lnot Q, close={:!u,!c}]
          [\lnot R,  close={:not conc,!c}, just={$\lif$ Elim:last premise}]]
        [\lnot R, close={:not conc,!c}, move by=1, just={$\vee$ Elim:!u}]]]]]]
\end{prooftree}
\end{codcoeden}

这棵树最终看起来像这样：

Answer 1

要排版树本身，您只需加载prooftrees前导码并定义树的特定内容所需的任何特殊符号。在这种情况下\lif是非标准的，我们需要turnstile旋转门的包。

所以，

\documentclass[border=10pt,tikz,multi]{standalone}
\usepackage{prooftrees,turnstile}
\newcommand*{\lif}{\ensuremath{\mathbin{\rightarrow}}}
\begin{document}
\begin{prooftree}
{
to prove={\{P \vee (Q \vee \lnot R), P \lif \lnot R, Q \lif \lnot R\} \sststile{}{} \lnot R}
}
[P \vee (Q \vee \lnot R),  just=Ass, checked
[P \lif \lnot R,  just=Ass, checked
  [Q \lif \lnot R,  just=Ass, checked, name=last premise
    [\lnot\lnot R, just={$\lnot$ Conc}, name=not conc
      [P,  just={$\vee$ Elim:!uuuu}
        [\lnot P, close={:!u,!c}]
        [\lnot R,  close={:not conc,!c}, just={$\lif$ Elim:!uuuu}]]
      [Q \vee \lnot R
        [Q, move by=1
          [\lnot Q, close={:!u,!c}]
          [\lnot R,  close={:not conc,!c}, just={$\lif$ Elim:last premise}]]
        [\lnot R, close={:not conc,!c}, move by=1, just={$\vee$ Elim:!u}]]]]]]
\end{prooftree}
\end{document}