계획 증명 트리

Question

저는 현재 구성표의 정규식에 대한 증명 트리를 만드는 작업 중입니다. 내가 수강하는 과정에서 제안된 이러한 작성 방법은 다음과 같습니다. 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}