bussproofs
The bussproofs extension implements the bussproofs
style package from
LaTeX. See the CTAN page for
more information and documentation of bussproofs.
Note that there are a couple of important differences between the use
of the package in MathJax compared to actual LaTeX. First, proofs
always have to be in a prooftree environment, i.e., inference macros
are only recognised if they are enclosed in \begin{prooftree}
and
\end{prooftree}
. Consequently the \DisplayProof
command is not
necessary.
Second, unlike in the LaTeX package, options for abbreviated inference
rule macros do not have to be manually set. All abbreviated macros are
directly available. Thus commands like \BinaryInfC
and \BIC
can be used immediately and interchangeably.
For example:
\begin{prooftree}
\AxiomC{}
\RightLabel{Hyp$^{1}$}
\UnaryInfC{$P$}
\AXC{$P\to Q$}
\RL{$\to_E$}
\BIC{$Q^2$}
\AXC{$Q\to R$}
\RL{$\to_E$}
\BIC{$R$}
\AXC{$Q$}
\RL{Rit$^2$}
\UIC{$Q$}
\RL{$\wedge_I$}
\BIC{$Q\wedge R$}
\RL{$\to_I$$^1$}
\UIC{$P\to Q\wedge R$}
\end{prooftree}
Also note that the bussproofs commands for sequent calculus derivations are not yet fully implemented.
This extension is loaded automatically when the autoload extension
is used. To load the bussproofs extension explicitly, add
'[tex]/bussproofs'
to the load
array of the loader
block
of your MathJax configuration, and add 'bussproofs'
to the
packages
array of the tex
block.
window.MathJax = {
loader: {load: ['[tex]/bussproofs']},
tex: {packages: {'[+]': ['bussproofs']}}
};
Alternatively, use \require{bussproofs}
in a TeX expression to
load it dynamically from within the math on the page, if the require
extension is loaded.
bussproofs Commands
The bussproofs extension implements the following macros:
\alwaysDashedLine
, \alwaysNoLine
, \alwaysRootAtBottom
, \alwaysRootAtTop
, \alwaysSingleLine
, \alwaysSolidLine
, \AXC
, \Axiom
, \AxiomC
, \BIC
, \BinaryInf
, \BinaryInfC
, \dashedLine
, \fCenter
, \LeftLabel
, \LL
, \noLine
, \QuaternaryInf
, \QuaternaryInfC
, \QuinaryInf
, \QuinaryInfC
, \RightLabel
, \RL
, \rootAtBottom
, \rootAtTop
, \singleLine
, \solidLine
, \TIC
, \TrinaryInf
, \TrinaryInfC
, \UIC
, \UnaryInf
, \UnaryInfC
And the following environments:
prooftree