Natural deduction and sequent proofs (Gentzen style)
- The best, most flexible package, is surely now bussproofs.sty (Sam Buss: download the latest version, 1.1, June 2011). Note that there is a LaTeX for Logicians User Guide to bussproofs.sty.
- An older, less flexible but still highly functional, alternative is provided by proof.sty (Makoto Tatsuta, originally 1990, and now in version 3.1). Again there is an old LaTeX for Logicians User Guide to proof.sty.
- Another older available package prooftree.sty (Paul Taylor, 1996)
- mathpartir provides the mathpar environment, a “paragraph mode for formulas”, and also the inferrule macro designed to typeset inference rules (Didier Rémy 2005)
- More flexibly (but probably also requiring a more sophisticated user), there is now Derivation trees with MetaPost (Laurent Méhats, 2010 — these don’t need a knowledge of MetaPost to use).
For Fitch-style layouts, there are also three packages
- The best is fitch.sty (Johan Klüwer, 2003): there is also a short guide to this package (Ang Tong, 2005)
- Alternatives producing similar output are fitch.sty (Peter Selinger, 2002) and fitch.sty (Delia Graff, 2001).