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, three, four or five 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. Subsequently, Peter Smith has written
wrote a thorough set of documentation which is highly recommended
(July 2004, updated March 2012). Peter deserves a huge thanks for this!
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 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.1, updated June 3, 2011.
-
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 documentation can be found Peter Smith's websites
in the LaTeX for Logicians web pages at Logic Matters, or
directly via LaTeX for Logicians,
in the section with macros for natural deduction proofs.
-
testbp2.tex - A sample LaTeX file. Originally
intended for testing purposes, so it's 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