Software: LaTeX style file

BUSSPROOFS.STY

bussproofs.sty is a LaTeX style file for constructing proof trees.   It was originally intended displayingl for sequent calculus proofs and natural deduction proofs but could be used for other purposes as well.    The kinds of features it supports include:

• Aligning formulas with connectives, such as the sequent arrow, vertically aligned.
• Inferences with zero, one, two or three hypotheses.
• Labeling inferences on either the left or the right or both.
• Shifting formulas horizontally to aid fitting them into the width of a page.
• Using different style lines to separate inferences.  Supported line styles are dotted, dashed and solid; also lines can be doubled or omitted.
• Proofs can be displayed in a prooftree environment, or can be used in line (anywhere an \hbox can be used).
• Proofs can be rendered with the root (conclusion) at either the bottom or the top.
• Has been tested (and works) with both LaTeX and plain TeX.

Documentation: The original documentation consisted only of comments at the beginning of the bussproofs.sty file. For more advanced features, read the beginning parts of the source code down to the end of the user-modifiable parameters.  However,  in July 2004, Peter Smith wrote a thorough set of documentation which is highly recommended. In addition, the sample LaTeX and postscript/PDF files available below show short examples of the kinds of proof trees that can be created. The only feature missing from Peter Smith's documentation is the ability to make proofs be "upside-down".

The bussproofs package is available through CTAN. (In CTAN releases after late 2006.)

Files are also available for download here: The current version is version 1.0, updated June 25, 2006.

• bussproofs.sty - The LaTeX style file.  See first part for comments that document its functionality.
• Peter Smith's documentation. This documentation is highly recommended.. The URL may change and if so, the documentation can be found Peter Smith's LaTeX for Logician's pages, in the section with macros for sequent calculus and natural deduction proofs. Lacks only documentation \rootAtTop and \alwaysRootAtTop and related commands.
• testbp2.tex - A sample LaTeX file.  Originally intended for testing purposes, so its not very user-friendly, but it does let you see some examples of how to use the macros. The output of the sample LaTeX file is available in postscript format or PDF format. 

Archives:  The style file and the testbp2 files are available in a zip archive, bussproofs.zip.

Author: Sam Buss