Sciweavers

AIML
2006

Deep Sequent Systems for Modal Logic

13 years 5 months ago
Deep Sequent Systems for Modal Logic
We see a systematic set of cut-free axiomatisations for all the basic normal modal logics formed by some combination the axioms d, t, b, 4, 5. They employ a form of deep inference but otherwise stay very close to Gentzen's sequent calculus, in particular they enjoy a subformula property in the literal sense. No semantic notions are used inside the proof systems, in particular there is no use of labels. All their rules are invertible and the rules cut, weakening and contraction are admissible. All systems admit a straightforward terminating proof search procedure as well as a syntactic cut elimination procedure. Keywords nested sequents
Kai Brünnler
Added 30 Oct 2010
Updated 30 Oct 2010
Type Conference
Year 2006
Where AIML
Authors Kai Brünnler
Comments (0)