Modular Sequent Systems for Modal Logic

We see cut-free sequent systems for the basic normal modal logics formed by any combination the axioms d, t, b, 4, 5. These systems are modular in the sense that each axiom has a corresponding rule and each combination of these rules is complete for the corresponding frame conditions. The systems are based on nested sequents, a natural generalisation of hypersequents. Nested sequents stay inside the modal language, as opposed to both the display calculus and labelled sequents. The completeness proof is via syntactic cut elimination.

• Type: Conference
• Year: 2009
• Where: TABLEAUX
• Authors: Kai Brünnler, Lutz Straßburger
• Keywords: Artificial Intelligence, Cut-free Sequent Systems, Nested Sequents, Normal Modal Logics, TABLEAUX 2009