[isabelle] New AFP entry: Invertibility in Sequent Calculi by Peter Chapman

Title:  	Invertibility in Sequent Calculi
Author: 	Peter Chapman

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.


For users of Nominal Isabelle I recommend the subtheory NominalSequents.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.