☰

证明树中的垂直对齐

tag-icon • tag-icon logic proof-package bussproofs logicproof
证明树中的垂直对齐

我尝试了几个软件包来对齐推理规则，但我还没有弄清楚如何避免以下问题。我的证明树如下所示：

           A
-------------------------  
  B                
-----  
  D                 C

但应该看起来像这样：

           A
-------------------------  
  B                C  
-----  
  D

您对支持该对齐的软件包有什么建议吗？具体来说，我可以用 \infer 来实现这一点吗？我尝试包含一个最小工作示例，但当我最小化证明树时，它甚至不再适用于上述情况，我似乎无法弄清楚原因。我还尝试了 bussproofs，但没有成功。

答案1

对于您正在绘制的证明类型，您需要指示bussproofs将树倒置。这可以通过命令完成\rootAtTop。如果您的所有证明都像这样，那么您可以使用序言中的命令全局设置根\alwaysRootAtTop，在这种情况下，您不需要为每个证明指定它。

\documentclass{article}
\usepackage{bussproofs}
\begin{document}
\begin{prooftree}
\rootAtTop
  \AxiomC{D}
  \UnaryInfC{B}
  \AxiomC{C}
  \BinaryInfC{A}      
\end{prooftree}
\end{document}

代码输出

答案2

的较新替代方案bussproofs是ebproof。这基本上是为了克服和 中的某些限制bussproofs而编写的，因为它的作者不喜欢 的bussproofs设计中实现的所有决定。

ebproof使用内联和显示证明的示例：

ebproof 内联和显示

\documentclass{article}
\usepackage{ebproof}
\begin{document}
\begin{prooftree}
  [proof style=downwards]
  \hypo{D}
  \infer1{B}
  \hypo{C}
  \infer2{A}
\end{prooftree}
\begin{prooftree}*
  [proof style=downwards]
  \hypo{D}
  \infer1{B}
  \hypo{C}
  \infer2{A}
\end{prooftree}
\end{document}

但是，我建议为所需的符号定义语义标记，并避免直接使用手册\vdash中的名称。或者，使用包。ebproofturnstile

相关内容