LaTeX for Logicians

Setting natural deduction tree proofs

There are a number of packages available for setting out sequent proofs/natural deduction proofs in Gentzen/Prawitz style.

proof.sty (Makoto Tatsuta, originally 1990, and now in version 3.0).
- A User Guide to proof.sty

A derivation of one of De Morgan's Laws, set using proof.sty

prooftree.sty (Paul Taylor, 1996: bug fix due to Chung-chieh Shan, which fixes a bug related to long rule-names).
bussproofs.sty (Sam Buss, 2001-2004: download the latest version, 0.7, July 2004)
- A User Guide to bussproofs.sty (PDF)

The two styles of sequent alignment available in bussproofs.sty

All three packages have been recommended by users. As the User Guides show, Makoto Tatsuta's package is both less flexible and more awkward to use than Sam Buss's. So in general the latter is to be preferred.

Home