In structural proof theory, the nested sequent calculus is a reformulation of the sequent calculus to allow deep inference.[1]
 | This mathematical logic–related article is a stub. You can help Wikipedia by adding missing information. |
logic, sequent calculus is a style of formal logical argumentation in which every line of a proof is a conditional tautology (called a sequent by Gerhard
theory comes from a technical notion introduced in the sequent calculus: the sequent calculus represents the assertion made at any stage of an inference
Weisstein, Eric W. "Sequent Calculus". Wolfram MathWorld. Retrieved 9 August 2025. "Interactive Tutorial of the Sequent Calculus". logitext.mit.edu. Retrieved
deduction. For this reason he introduced his alternative system, the sequent calculus, for which he proved the Hauptsatz both for classical and intuitionistic
analytic proof was introduced by Gentzen for the sequent calculus, where he proved that the sequent calculus of classical and intuitionistic logics are cut-free
However, a nested metalanguage differs from an ordered one in that each level includes the one below. The paradigmatic example of a nested metalanguage
negative polarity. Many other sequent calculi has been shown to have the focusing property, notably the nested sequent calculi of both the classical and
Olivetti, Nicola; Pozzato, Gian Luca; Schwind, Camilla B. (2007). "A Sequent Calculus and a Theorem Prover for Standard Conditional Logics". ACM Transactions
