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.
Two ways of aligning sequents provided by Bussproofs
- 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.
A derivation of one of De Morgan's Laws, set using 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).
Set using Klüwer's version of fitch.sty
Other packages
- The Virginia Lake package offers macros aimed at “writing papers in the area of deep inference and the calculus of structures” but which could be adopted for other proof theoretic purposes.
- The flagderiv package can be used to set the variant kind of “flag” proofs some computer scientists like.