# What is the best package out there to typeset proof trees?

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?

-
I'm quite sure how the trees should look like (maybe you could add an actual picture), but does anything from chapters 17 ("Making Trees Grow") and 42 ("Tree Library") of the TikZ manual (ctan.org/tex-archive/graphics/pgf/base/doc/generic/pgf/…) look like what you want? –  Caramdir Jul 28 '10 at 14:34
Sorry, I thought my sketch was already explicit enough, but I've just discovered that people draw trees in many different ways! Anyway, I've just added a picture of the kind of trees I want. –  Juan A. Navarro Jul 28 '10 at 15:43

Peter Smith's very useful LaTeX for Logicians page offers suggestions both for downward branching proof-trees and 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}

-
Thanks for the link, but I'm looking for something more like "natural deduction proofs" (I've clarified the question). Also for completeness please include the answer here, as well as linking to the external resource. This helps the answer live even if the external link goes down in the future. –  Juan A. Navarro Jul 28 '10 at 13:19
Actually on your second link I did found something that looks like what I'm looking for! It's under Natural deduction proofs. If possible, please update your answer to contain the answer and not just a pointer to answer. –  Juan A. Navarro Jul 28 '10 at 15:56
Done(ish). I brought in only Smith's top choice. I did not want to steal Smith's thunder and I do think anyone working in logic with LaTeX ought to know his page. If the downvote was yours, perhaps you might undo it? Also, while I take your point about the fragility of purely external references and think the image in your question now makes your desire quite clear, what happens to this question if you stop maintaining your site hosting the picture? –  vanden Jul 28 '10 at 16:11
Exactly! And that's why we're having this discussion here meta.tex.stackexchange.com/questions/119/where-should-images-go –  Juan A. Navarro Jul 28 '10 at 16:35

I like mathpartir (by Didier Remy) for its simple and flexible design, and smart layout concept. The name stands for "math formulas in paragraph mode" and "typesetting inference rules". You can use it to typeset a number of rule definitions. For example:

\begin{mathpar}
\inferrule[Foo]{A \\ B \\\\ C}{D}
\and
\inferrule[Bar]{X}{Y}
\end{mathpar}


You can also typeset a derivation tree:

$\inferrule* [left=Total] {\inferrule* [Left=Foo] {\inferrule* [Right=Bar, leftskip=2em,rightskip=2em,vdots=1.5em] {a \\ a \\\\ bb \\ cc \\ dd} {ee} \\ ff \\ gg} {hh} \\ \inferrule* [lab=XX]{uu \\ vv}{ww}} {(1)}$


-
This one is the best! –  day Aug 7 '11 at 14:39

Another question I missed. I began to use Paul Taylor's proof trees macros for my doctoral dissertation, but it has a bug that occurs when you want to use it with labels. This led me to write my own proof trees macros, which worked well enough. I should probably publish them one of these days.

Since then I've used Buss's macros, which are as good as any, although the stack metaphor for writing proof trees is not as intuitive as the grouping-oriented one of Paul Taylor's. But this is a very slight complaint.

All packages I've seen have one problem: they use Tex's boxes to set subdervivations, which means that they leave far too much space for many derivations, because they can't see that one subderivation could sit "in the shadow" of another. Sometimes this looks odd, sometimes it means you can't set large derivations without reducing font size. With negative horizontal spce, one can fix this, but this is a workaround.

The Right Thing is not to use boxes but trees to calculate how far apart to position the conclusion of subderivations. This can be done without much difficulty in Metapost —I'm not sure about PGF— and implementing this in Luatex library is on my list of rainy day projects.

-

Though not originally designed for proof trees, the synttree package is very nice and easy for drawing trees.

Also check out this page on Tree Drawing in LaTeX.

-
Thanks for the answer, but I was looking for something more like "natural deduction proofs", i've added to the question a sketch of what I mean. –  Juan A. Navarro Jul 28 '10 at 13:16
Though this isn't what the OP wanted, it's a good answer. Personally, I always use [qtree][essex.ac.uk/linguistics/external/clmt/latex4ling/trees/qtree/], which I also discovered from that site you linked to :-) –  TJ Ellis Jul 28 '10 at 13:58

I have been using Paul Taylor's proof-tree package combined with some macros I have written myself. I have used the package for typeset proofs in papers, slides, my MSc thesis, problem sets and solutions.

A simple example follows:

\documentclass{article}
\usepackage{prooftree}
\begin{document}
\begin{prooftree}
$\[ A \justifies B$
C
\justifies
D
\]
$\[ E \quad F \justifies G$