Deep sequent systems for modal logic |
| |
Authors: | Kai Brünnler |
| |
Institution: | (1) Institut für Angewandte, Mathematik und Informatik, Neubrückstr. 10, 3012 Bern, Switzerland |
| |
Abstract: | 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 Modal logic Cut elimination Deep inference |
本文献已被 SpringerLink 等数据库收录! |
|