我可以在 ConTeXt 中排版特定的证明树吗？

Question

现在我知道了下面的图片可以用 LaTeX 完成。可以在 ConTeXt 中完成吗？因为我还没有学习任何 TeX 系统，所以我不会问如何在 ConTeXt 中做到这一点，但我主要想知道这是否可行。或者，我应该问 ConTeXt 是否可以做 LaTeX 能做的一切？

Answer 1

我适应了egreg 的回答并将其移植到 ConTeXt。在这种情况下这是可行的，因为bussproofs编写的版本也兼容纯 TeX，这使得它更容易。不幸的是，的开发人员bussproofs认为定义自己的版本是个好主意\newcount，结果在示例的前几行中出现了这个丑陋的 hack。

如果宏中的斜线\cancel太不明显，请/在\cancel宏中用替换\backslash。

\catcode`\@=11
% Ugly hackery to make the own definition of \newcount in bussproofs work
\countdef\insc@unt=20
\countdef\allocationnumber=21
\def\alloc@#1#2#3#4#5{\global\advance\count1#1by\@ne
  \allocationnumber=\count1#1%
  \global#3#5=\allocationnumber
  \wlog{\string#5=\string#2\the\allocationnumber}}
\catcode`\@=12

\input bussproofs.sty

\def\lto{\mathbin{\to}}
\catcode`\@=11
\def\cancel#1{\mathpalette\cancel@{#1}}
\def\cancel@#1#2{{\ooalign{%
      $#1#2$\cr
      \hidewidth$#1/$\hidewidth\cr}%
  }}
\def\circled#1{\mathpalette\circled@{#1}}
\def\circled@#1#2{{\ooalign{%
      $#1\bigcirc$\cr
      \hidewidth\lower.125ex\hbox{$#1#2$}\hidewidth\cr}%
  }}
\catcode`\@=12

\starttext

\def\defaultHypSeparation{\hskip 4em}
\AxiomC{${\cancel{\psi}}^{\circled{1}}$}
\AxiomC{$(\phi\land\psi)$}
\RightLabel{($\land\rm{E}$)}
\UnaryInfC{$\phi$}
\RightLabel{($\land\rm{I}$)}
\BinaryInfC{$(\psi\land\phi)$}
\LeftLabel{$\circled{1}$}
\RightLabel{($\lto\rm{I}$)}
\UnaryInfC{$(\psi\lto(\psi\land\phi))$}
\DisplayProof

\stoptext