Draft:Bussproofs
 | Draft article not currently submitted for review.
This is a draft Articles for creation (AfC) submission. It is not currently pending review. While there are no deadlines, abandoned drafts may be deleted after six months. To edit the draft click on the "Edit" tab at the top of the window. To be accepted, a draft should:
It is strongly discouraged to write about yourself, your business or employer. If you do so, you must declare it. Where to get help
How to improve a draft
You can also browse Wikipedia:Featured articles and Wikipedia:Good articles to find examples of Wikipedia's best writing on topics similar to your proposed article. Improving your odds of a speedy review To improve your odds of a faster review, tag your draft with relevant WikiProject tags using the button below. This will let reviewers know a new draft has been submitted in their area of interest. For instance, if you wrote about a female astronomer, you would want to add the Biography, Astronomy, and Women scientists tags. Editor resources
Last edited by Miminity (talk | contribs) 2 seconds ago. (Update) |
 | This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these messages)
|
| Original author(s) | Samuel R. Buss |
|---|---|
| Initial release | 1990s |
| Written in | LaTeX |
| Operating system | Cross-platform |
| Platform | TeX |
| Type | Typesetting |
| License | LaTeX Project Public License |
| Website | ctan.org/pkg/bussproofs |
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
[edit]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
[edit]- 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
[edit]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
[edit]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
[edit]References
[edit]External links
[edit]