# 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.

Short addition: For those who like bussproofs for the generated output, but would rather prefer not to use the stack-based syntax, I've written a frontend for bussproofs allowing for the specification of proofs in an easy lisp-like syntax. Within this syntax, you can define custom operators including precedence information (such that the addition of parentheses is also handled by the tool). Proof are specified starting from the root, which also might be more intuitive for some people; still, they are rendered in the usual leaves-to-root manner.

Example input:

(macro implies 0 "\Longrightarrow")
(defop neg "\neg " 40 prefix)
(defop modality "\left[#1\right]#2" 40 param)
(defop land " \land " 30 infix)
(defop text "\textrm{#1}" 99999 param)
(defop list ", " 10 infix)
(defop lor " \lor " 20 infix)
(defop seq "\implies  " 0 infix)

(proof (
(lor  "asdf" (lor  "asdf" (neg  "asdf")))
(seq  "" (modality  "p" "\phi"))
(neg  (lor  "p" "q"))
(land  (lor  "p" "q") (lor  "q" "p"))
(lor  (land  "p" "q") (land  "q" "p"))
(lor  "asdf" (lor  "asdf" "asdf")) <- "That's a'' right label!"
"FancySplitRule 1" -> (seq  "" (list  (neg  "p") (neg  "q") (lor  "p" "q")))
(
"subtree1"
"test"
(
"test"
(seq  (lor  "p" (neg  "q")) "succedent")
(neg  "p")
)
)
(
"subtree2"
"test"
)
(
(text  "And a third branch!!!")
)
))


which would be rendered to:

using, for instance, a one-liner as the following one (for the fish shell):

java -jar ProofRenderer.jar -f $argv[1].pt -r standalone-latex -o$argv[1].tex -a "--fit-to-page" ; and pdflatex -interaction=batchmode \$argv[1].tex


Advantages are the variable degree of abstraction (you can have plain LaTeX in a String and only define the structure by lisp brackets, or you can define a lot of macros and operations and have a tree with lisp-like elements only), the root-to-leaves notation which is still rendered as usual, and the extensibility to different renderers. A disadvantage is that you need yet another tool and cannot include it into your source code directly. Feel free to try it out ;)

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

• 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$
\justifies
H
\]
\justifies
J
\end{prooftree}
\end{document}


People who need to typeset lots of trees may want to take a look at Dednat6, that understands 2D ascii art trees in blocks of comments. Dednat6 is not at CTAN yet, but there is a TUGBoat article about it.

The following LuaLaTeX code

%:                       H
%:                      ...
%:  A  B  C   E  F      \Pi
%:  =======r  ::::\phi  ...
%:     D       G         I
%:     -------------------
%:             J
%:
%:             ^demo
%:
\pu
$$\ded{demo}$$


is rendered as:

To me, ebproof is definitely the way to go.

As the author of the package writes,

The structure is very much inspired by the bussproofs package, in particular for the postfix notation. I actually wrote ebproof because there were some limitations in bussproofs that I did not know how to lift, and also because I did not like some choices in that package (and also because it was fun to write).

The following code:

\documentclass[border=10pt]{standalone}
\usepackage{ebproof}
\begin{document}
\begin{prooftree}
\hypo{A}
\infer1{B}
\hypo{C}
\infer2{D}
\hypo{E}
\hypo{F}
\infer2{G}
\infer1{H}
\infer2{J}
\end{prooftree}
\end{document}


produces:

But the package allows many subtle modifications regarding style, alignment, labels, etc., making it the most modular option I am aware of.

• A note to anyone else using this package - I initially thought \infer2{} referred to the "level" of the statement, but it actually refers to the amount of children the statement has. – James Paterson Mar 28 at 18:44