Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Invertibility in Sequent Calcul...

view this post on Zulip Email Gateway (Aug 18 2022 at 13:58):

From: Tobias Nipkow <nipkow@in.tum.de>
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.

http://afp.sourceforge.net/entries/SequentInvertibility.shtml

For users of Nominal Isabelle I recommend the subtheory NominalSequents.

Enjoy!
Tobias

Last updated: Apr 20 2024 at 08:16 UTC