Busproofs 树无法编译

Question

我有以下证明树，LaTeX 说其指定不正确。

这是 TeX。

\documentclass{article}
\usepackage{bussproofs}
\usepackage{amsmath}
\begin{document}
\begin{prooftree}
\AxiomC{$Sz + t = 0 \dagger$} \AxiomC{$t = 0 \dagger$}
\BinaryInfC{$Sz + 0 = 0$}                                   \AxiomC{$Sz + 0 = Sz$}
                                \BinaryInfC{$Sz = 0$}                                   \AxiomC{$\neg (Sz = 0)$}
                                                        \BinaryInfC{$\bot$}
                                                        \UnaryInfC{$\neg(Sz + t) = 0$}





\AxiomC{$\neg(t = 0)$}
\UnaryInfC{$\exists w (t = Sw)$}    
                                                \AxiomC{$t = Sy \dagger$}   \AxiomC{$Sz + t = 0 \dagger$}
                                                        \BinaryInfC{$S(z + y) = 0$}                     \AxiomC{$\neg(S(z + y) = 0$}
                                                                                    \BinaryInfC{$\bot$}
                                                                                    \UnaryInfC{$\neg(Sz + t = 0)$}


\BinaryInfC{$\neg(Sz + t) = 0$}
\end{prooftree}
\end{document}

有两棵证明树，都有结论$\neg(Sz + t = 0)$，我想把它们连接在一起得出结论$\neg(Sz + t = 0)$。我测试了一下，似乎错误出在第二棵树上（如果我删除第二棵树和结论，它就会起作用），但我找不到它。

Answer 1

基本问题是，当您给出\UnaryInfC最后一行时，第二个子树中有两个活动分支，这是行不通的，因为当您\BinaryInfC在最后一行发出时，您有三个活动分支。

代码可以通过多种方式进行编译，但如果不了解所用语言的语义和语法，就不可能知道哪种方式是正确的。

这是一种方法，仅作为一个例子。

\documentclass{article}
\usepackage{bussproofs,geometry}
\usepackage{amsmath}
\begin{document}
\begin{prooftree}
  \AxiomC{$Sz + t = 0 \dagger$} \AxiomC{$t = 0 \dagger$}
  \BinaryInfC{$Sz + 0 = 0$}                                   \AxiomC{$Sz + 0 = Sz$}
  \BinaryInfC{$Sz = 0$}                                   \AxiomC{$\neg (Sz = 0)$}
  \BinaryInfC{$\bot$}
  \UnaryInfC{$\neg(Sz + t) = 0$}

  \AxiomC{$\neg(t = 0) \dagger$}
  \UnaryInfC{$\exists w (t = Sw)$}    
  \UnaryInfC{$t = Sy$}   
  \AxiomC{$Sz + t = 0 \dagger$}
  \BinaryInfC{$S(z + y) = 0$}                     
  \AxiomC{$\neg(S(z + y) = 0$}
  \BinaryInfC{$\bot$}
  \UnaryInfC{$\neg(Sz + t = 0)$}

  \BinaryInfC{$\neg(Sz + t) = 0$}
\end{prooftree}
\end{document}