Last active
November 1, 2024 00:12
-
-
Save jedavidson/9913d5767c6d2514ceed75c0158cda5c to your computer and use it in GitHub Desktop.
An example of how to use the bussproofs.sty file for setting out proof trees.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
% I'm assuming you have the package imported already | |
\usepackage{bussproofs} | |
% In these examples, I like indenting the InfC part of each proof tree from the AxiomC(s) that spawned it, | |
% and keeping those AxiomC(s) on the same indent level, but I keep the bottom, final InfC unindented | |
% This is a personal choice but it makes it easier to keep track of what's happening for large trees | |
% A rule with no assumptions (i.e. an axiom) | |
\begin{prooftree} | |
\AxiomC{} | |
\UnaryInfC{$A$ \textbf{Foo}} | |
\end{prooftree} | |
% A rule with one assumption | |
\begin{prooftree} | |
\AxiomC{$A$ \textbf{Foo}} | |
\UnaryInfC{$f(A)$ \textbf{Foo}} | |
\end{prooftree} | |
% A rule with two assumptions | |
% Note how UnaryInfC changed to BinaryInfC; read the docs for more info | |
\begin{prooftree} | |
\AxiomC{$A_1$ \textbf{Foo}} | |
\AxiomC{$A_2$ \textbf{Foo}} | |
\BinaryInfC{$f(A_1) + f(A_2)$ \textbf{Foo}} | |
\end{prooftree} | |
% A rule with the top assumptions being proof trees themselves | |
% You can keep doing this for as long as you like, just be careful with the LaTeX | |
\begin{prooftree} | |
\AxiomC{} | |
\UnaryInfC{$A_1$ \textbf{Foo}} | |
\AxiomC{} | |
\UnaryInfC{$A_2$ \textbf{Foo}} | |
\BinaryInfC{$f(A_1) + f(A_2)$ \textbf{Foo}} | |
\end{prooftree} | |
% Naming a rule with a label on the right | |
\begin{prooftree} | |
\AxiomC{} | |
\RightLabel{$R$} | |
\UnaryInfC{$A$ \textbf{Foo}} | |
\end{prooftree} | |
% Aligning multiple proof trees | |
% If you're attempting to fit too many trees on a line it will break them apart, so be careful | |
\begin{prooftree} | |
\AxiomC{} | |
\UnaryInfC{$A$ \textbf{Foo}} | |
\DisplayProof \hskip 1em | |
\AxiomC{} | |
\UnaryInfC{$B$ \textbf{Foo}} | |
\DisplayProof \hskip 1em | |
\AxiomC{} | |
\UnaryInfC{$C$ \textbf{Foo}} | |
\end{prooftree} | |
% Aligning multiple proof trees correctly which are 'vertically uneven' using vphantom | |
\begin{prooftree} | |
\AxiomC{$A_1$ \textbf{Foo}} | |
\AxiomC{$A_2$ \textbf{Foo}} | |
\BinaryInfC{$f(A_1) + f(A_2)$ \textbf{Foo}} | |
\DisplayProof \hskip 1em | |
% This proof tree here contains no assumption so the final inference line will be uneven | |
% with the previous tree's final inference line; so we place the content of an assumption | |
% in a \vphantom environment which creates a zero-width box of the same height as what | |
% you pass in, in this case the rule from that first tree | |
\AxiomC{\vphantom{$A_1$ \textbf{Foo}}} | |
\UnaryInfC{$A$ \textbf{Foo}} | |
\end{prooftree} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment