我目前正在研究如何为 Scheme 中的正则表达式制作证明树。我所学课程中建议的编写方法如下，我已手动将其输入到 TeX 中。
然而，这是一个繁琐的过程，尤其是对于长表达式。所以我正在寻找一种巧妙的方法来制作上面显示的证明树类型，或者可能是一种可以完成相同功能的替代方法。
编辑：
这是我的代码，我不介意输入树，但这种方式真的非常非常慢。所以如果有一个包可以为我做一些定位工作，我会很高兴。
\phantom{ATOM}\ \ \ \ \ 1 is a Scheme integer\qquad\qquad\qquad (\%regexp (atom 2))\\
ATOM ---------------------\qquad\qquad SEQ ------------------------------------------------------------\\
\phantom{ATOM} (\%regexp (atom 1)) \qquad\qquad\qquad\ \ (\%regexp (seq (atom 2) (seq (atom 3) (seq (atom 4) (empty)))\\
\phantom{A}SEQ ---------------------------------------------------------------------------------------------\\
\phantom{ATOM} (\%regexp (seq (atom 1) (seq (atom 2) (seq (atom 3) (seq (atom 4) (empty))))))
编辑2：
我还没有找到有关该bussproofs软件包的解决方案，但它仍然不是最佳的，当证明树变大时它看起来有点奇怪。
我创建这个的代码是：
\begin{prooftree}
\def\ScoreOverhang{1pt}
\def\extraVskip{6pt}
\def\defaultHypSeparation{\hskip .2in}
\def\ruleScoreFiller{\hbox to1.1mm{\hss\vrule width0.9mm height0.4pt depth0.0pt\hss}}
\AxiomC{1 is a Scheme integer}
\LeftLabel{ATOM}
\UnaryInfC{(\%regexp (atom 1))}
\AxiomC{2 is a Scheme integer}
\LeftLabel{ATOM}
\UnaryInfC{(\%regexp (atom 2))}
\AxiomC{3 is a Scheme integer}
\LeftLabel{ATOM}
\UnaryInfC{(\%regexp (atom 3))}
\AxiomC{4 is a Scheme integer}
\LeftLabel{ATOM}
\UnaryInfC{(\%regexp (atom 4))}
\AxiomC{}
\LeftLabel{EMPTY}
\UnaryInfC{(\%regexp (empty))}
\LeftLabel{SEQ}
\BinaryInfC{(\%regexp (seq (atom 4) (empty)))}
\LeftLabel{SEQ}
\BinaryInfC{(\%regexp (seq (atom 3) (seq (atom 4) (empty))))}
\LeftLabel{SEQ}
\BinaryInfC{(\%regexp (seq (atom 2) (seq (atom 3) (seq (atom 4) (empty)))))}
\LeftLabel{SEQ}
\BinaryInfC{(\%regexp (seq (atom 1) (seq (atom 2) (seq (atom 3) (seq (atom 4) (empty))))))}
\end{prooftree}