Invertibility in Sequent Calculi

Peter Chapman

August 28, 2009

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


The invertibility of the rules of a sequent calculus is important for guiding proof search and can be used in some formalised proofs of Cut admissibility. We present sufficient conditions for when a rule is invertible with respect to a calculus. We illustrate the conditions with examples. It must be noted we give purely syntactic criteria; no guarantees are given as to the suitability of the rules.


GNU Lesser General Public License (LGPL)


Session SequentInvertibility