使用 busproofs 编写推理规则的紧凑方法

Question

我有以下推理规则

我需要用该包来编写bussproofs并在 mathjax 中使用它。

Mathjax 支持总线防护

我不知道如何用相同的形式重现以下推理规则，例如<A, []> -> []

为了编写这些规则，我使用了proof但它在 mathjax 上不可用

Answer 1

以下内容应bussproofs在 MathJax 中设置和运行你的证明：

\newcommand\inf[2]{$\langle#1,[]\rangle\rightarrow #2$}

\begin{prooftree}
  \AXC{}\RL{num}
  \UIC{\inf{1}{1}}
  \AXC{}\RL{var}
  \UIC{\inf{x}{0}}\RL{gt}
  \BIC{\inf{x>1}{false}}
  \AXC{}\RL{skip}
  \UIC{\inf{skip()}{[]}}\RL{if}
  \BIC{\inf{if(x>1)then(x:=10)else(skip())}{[]}}
\end{prooftree}

请注意，宏\inf设置了你的推理规则。