Generic modal cut elimination applied to conditional logics

Dirk Pattinson*, Lutz Schröder

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

7 Citations (Scopus)

Abstract

We develop a general criterion for cut elimination in sequent calculi for propositional modal logics, which rests on absorption of cut, contraction, weakening and inversion by the purely modal part of the rule system. Our criterion applies also to a wide variety of logics outside the realm of normal modal logic. We give extensive example instantiations of our framework to various conditional logics. For these, we obtain fully internalised calculi which are substantially simpler than those known in the literature, along with leaner proofs of cut elimination and complexity. In one case, conditional logic with modus ponens and conditional excluded middle, cut elimination and complexity are explicitly stated as open in the literature.

Original languageEnglish
Title of host publicationAutomated Reasoning with Analytic Tableaux and Related Methods - 18th International Conference, TABLEAUX 2009, Proceedings
Pages280-294
Number of pages15
DOIs
Publication statusPublished - 2009
Externally publishedYes
Event18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009 - Oslo, Norway
Duration: 6 Jul 200910 Jul 2009

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5607 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference18th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009
Country/TerritoryNorway
CityOslo
Period6/07/0910/07/09

Fingerprint

Dive into the research topics of 'Generic modal cut elimination applied to conditional logics'. Together they form a unique fingerprint.

Cite this