![使用 busproofs 编写推理规则的紧凑方法](https://linux22.com/image/435047/%E4%BD%BF%E7%94%A8%20busproofs%20%E7%BC%96%E5%86%99%E6%8E%A8%E7%90%86%E8%A7%84%E5%88%99%E7%9A%84%E7%B4%A7%E5%87%91%E6%96%B9%E6%B3%95.png)
我有以下推理规则
我需要用该包来编写bussproofs
并在 mathjax 中使用它。
Mathjax 支持总线防护
我不知道如何用相同的形式重现以下推理规则,例如<A, []> -> []
为了编写这些规则,我使用了proof
但它在 mathjax 上不可用
答案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
设置了你的推理规则。