seqcalc - A structured sequent calculus wrapper for bussproofs

Overview

Version: 1.0 Date: 2026-01-31 Author: Julian (lambdaphoenix) License: LPPL 1.3c or later

seqcalc is a structured, declarative wrapper around the bussproofs package. It provides an interface for building sequent calculus proofs while preserving the underlying layout logic of bussproofs.

The package adds:

• a declarative rule system with automatic macro generation,
• optional formula-list normalization,
• optional debug output,
• optional shortcut commands,
• optional built-in standard rule sets,
• wrapper environments for proof trees.

seqcalc does not modify the spacing, box construction, or layout algorithms of bussproofs. It only adds a structured interface on top.

Features

Sequent commands

• \seq{A}{B} - typeset a sequent
• \seqL{A}, \seqR{A} - left/right-only sequents
• Automatic normalization of formula lists (optional)

Axioms and premises

• \SeqAxiom{A} - closed leaf
• \SeqPremise{A} - open leaf

Conclusions

• \SeqConclusion[Label]{Cmd}{Formula}[Hint]
• Convenience forms:
  • \SeqConclusionU{Formula}
  • \SeqConclusionB{Formula}

Rule system

• Declare rules:

  \SeqCalcDeclareRule{Name}{Arity}[Label]
  

• Apply rules:

  \SeqRule{Name}{Formula}[Hint]
  \Name{Formula}[Hint]       % auto-generated
  

Shortcuts (optional)

• Enabled via:

  \EnableSeqShortcuts
  

### Standard rules (optional)

• Enabled via:

  \EnableSeqStandardRules
  

• seqproof - wrapper around prooftree
• seqproofinline - compact inline proof trees

Installation

Place seqcalc.sty somewhere in your TeX tree, then load it:

\usepackage{seqcalc}

Package options

Documentation

The full package documentation is available in:

• doc/seqcalc-doc.pdf
• Online: https://github.com/lambdaphoenix/seqcalc/blob/main/doc/seqcalc-doc.pdf

License

This work may be distributed and/or modified under the conditions of the LaTeX Project Public License, either version 1.3c of this license or (at your option) any later version. The latest version of this license is in    https://www.latex-project.org/lppl.txt and version 1.3c or later is part of all distributions of LaTeX version 2008 or later.

This work has the LPPL maintenance status maintained'. The Current Maintainer of this work is Julian.

Development

The package is developed openly on GitHub:  Repository: https://github.com/lambdaphoenix/seqcalc  Issue tracker: https://github.com/lambdaphoenix/seqcalc/issues