好的，我正在尝试证明建设性的困境：
\{p\lor q, p\to r, q\to r\} \vdash r
我尝试在 ebproofs 中为其建立一个证明树，但它给我带来了一些问题。
我的代码如下：
\begin{prooftree}
\Hypo{\neg r} \Hypo{p\to r} \Infer{2}[MT]{\neg p}
\Hypo{p\lor q} \Infer{2}[MT]{q}
\end{prooftree}
到目前为止一切正常。但是当我添加以下内容时：
\begin{prooftree}
\Hypo{\neg r} \Hypo{p\to r} \Infer{2}[MT]{\neg p}
\Hypo{p\lor q} \Infer{2}[MT]{q}
\Hypo{\neg r} \Hypo{p\to q} \Infer{2}[MT]{\neg q}
\end{prooftree}
我知道这是一个未完成的证明，但当我尝试运行代码时，出现了问题。显然，这是一个“畸形证明树”。
此处 MT = 撤销条件。
答案1
好吧，没关系。我找到了问题所在。结果发现，ebproofs 似乎无法运行部分证明。基本上，完成证明就解决了我遇到的问题。
\begin{prooftree}
\Hypo{\neg r} \Hypo{p\to r} \Infer{2}[MT]{\neg p}
\Hypo{p\lor q} \Infer{2}[MT]{q}
\Hypo{\neg r} \Hypo{p\to q} \Infer{2}[MT]{\neg q}
\Infer{2}[F]{\bot}
\end{prooftree}
就是这样...