[Tex/LaTex] the best package out there to typeset proof trees

logicpackages

So, I want to typeset some proof trees, i.e. trees of inference rules like those in natural deduction (see diagram below). Which are the best packages that you have found that allow you to do this, and which features do they have?

alt text

Best Answer

Peter Smith's very useful LaTeX for Logicians page offers suggestions both for downward branching proof-trees and for natural deduction proofs in both Gentzen sequent-style (the tree-like style you seem to be after) and Fitch-style.

I've not used any of the alternatives for proof trees, as I use Fitch-style natural deduction proofs. But, I've found Smith a most reliable guide and for your desire he recommends as best of breed Sam Buss's bussproofs.sty. Smith also has remarks about a few other alternatives that you might want to check out.

A quick example to produce your example tree would be:

\documentclass{article}
\usepackage{bussproofs}
\begin{document}
\begin{prooftree}
\AxiomC{A}
\UnaryInfC{B}
\AxiomC{C}
\BinaryInfC{D}
\AxiomC{E}
\AxiomC{F}
\BinaryInfC{G}
\UnaryInfC{H}
\BinaryInfC{J}
\end{prooftree}
\end{document}
Related Question