Invertibility in Sequent Calculi

 

Title: Invertibility in Sequent Calculi
Author: Peter Chapman
Submission date: 2009-08-28
Abstract: 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.
BibTeX:
@article{SequentInvertibility-AFP,
  author  = {Peter Chapman},
  title   = {Invertibility in Sequent Calculi},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2009,
  note    = {\url{http://isa-afp.org/entries/SequentInvertibility.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: GNU Lesser General Public License (LGPL)