Sequoia

Sequoia facilitates construction and analysis of sequent calculus proof systems for specification and meta-theoretical reasoning about logical calculi.

Key Features:

• Proof Construction: Accepts user-specified inference rules and constructs proof trees within defined sequent calculi.
• Meta-Theoretical Analysis: Automatically infers trivial cases for meta-theoretical properties including identity expansion, weakening admissibility, and permutability of rules.
• Custom Calculi Management: Supports creation, modification, and management of user-defined calculi.

Scientific Applications:

• Sequent Calculus Specification: Specifying and experimenting with sequent calculi to study rule structure and interactions.
• Meta-Theory Investigation: Analyzing admissibility and permutability properties such as identity expansion and weakening admissibility.
• Proof Development and Exploration: Constructing and examining proof trees to explore derivations and combinatorial behavior in logical systems.

Methodology:

Parses and renders user-specified inference rules, constructs proof trees, performs automated inference of trivial meta-theoretic cases (identity expansion, weakening admissibility, permutability), and supports basic reasoning about specified sequent calculi.