Sstrhsrtj

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)}

]

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[#1right]#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.

Also check out this page on Tree Drawing in LaTeX.

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 ]

  quad

  C 

  justifies

  D

]

quad

[ 

  [ E quad F justifies G ]

  justifies 

  H 

]

justifies

J

end{prooftree}

end{document}

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.