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

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}

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.