Bussproofs
| Original author(s) | Samuel R. Buss |
|---|---|
| Initial release | 1990s |
| Written in | Template:Linked TeX wordmark |
| Engine | |
| Operating system | Cross-platform |
| Platform | TeX |
| Type | Typesetting |
| License | LaTeX Project Public License |
| Website | ctan.org/pkg/bussproofs |
Search Bussproofs on Amazon.
Bussproofs is a LaTeX package add-on designed for typesetting natural deduction, sequent calculus, and other structured logical proofs in a clear, readable format. It was developed by Samuel R. Buss to facilitate the layout of formal proofs, particularly for use in mathematical logic, computer science, and philosophy.[1]
Overview
The package enables users to create vertically aligned, tree-like structures that represent logical deductions. Each inference step is visually aligned with its premises and conclusion, closely mirroring textbook-style proofs. It supports custom rule names, line labels, and both one-sided and two-sided proof layouts.
Features
- Tree-structured proof environments
- Adjustable line spacing and alignment
- Rule names and justifications above or beside inference bars
- Horizontal grouping for compact subproofs
- Compatibility with standard LaTeX math environments
Example
This LaTeX source:
\begin{prooftree}
\AxiomC{$P \rightarrow Q$}
\AxiomC{$P$}
\RightLabel{\scriptsize (Modus ponen)}
\BinaryInfC{$Q$}
\end{prooftree}
Would render approximately as:
P → Q P
──────────── (Modus Ponens)
Q
Use cases
The package is commonly used in:
- Logic textbooks and teaching materials
- Research papers in proof theory and formal logic
- Computer science publications involving formal verification or type theory
See also
References
External links
This article "Bussproofs" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:Bussproofs. Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.
