🚀 go-pugleaf

Hello.

I have been trying to produce natural deduction proof trees
using LaTeX or AMSTeX and quite simply cannot get it to work.

The proof trees in question are stacks, perhaps half a page long,
of formulae ( in so called "sequent" form) arranged in a tree.
A crude  and very simple example:

        A -> A                         B -> B
      --------- thinning              --------- thinning
       A -> A,B                        B -> A,B
       -------- Or-succ.              ---------- Or-succ.
       A -> A%B                        B -> A%B
      ----------------------------------------- And-antec.
                   A & B -> A, B

The problem is that the trees may not be 'balanced', the branches 
may be very different in size and number, and the formulas may be
very different in length.

My experiments so far have produced incredible garbage (in most cases)
but also some near-misses.  

Has anyone been able to do this properly?  With what tricks?

I would be very grateful for any good hints on how to do this, if 
anyone cares to help, please post or e-mail as you see fit,

Tryggvi Edwald, University of Iceland, te@rhi.hi.is (or ..!mcvax!hafro!rhi!te)