Generic Modal Cut Elimination Applied to Conditional Logics
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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2011-03-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/968/pdf |
| _version_ | 1797268766120214528 |
|---|---|
| author | Dirk Pattinson Lutz Schröder |
| author_facet | Dirk Pattinson Lutz Schröder |
| author_sort | Dirk Pattinson |
| collection | DOAJ |
| description | 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 were explicitly stated as open in the literature. |
| first_indexed | 2024-04-25T01:37:41Z |
| format | Article |
| id | doaj.art-69b489e64d5844f5b7508569f7aedcb5 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:37:41Z |
| publishDate | 2011-03-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-69b489e64d5844f5b7508569f7aedcb52024-03-08T09:14:52ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742011-03-01Volume 7, Issue 110.2168/LMCS-7(1:4)2011968Generic Modal Cut Elimination Applied to Conditional LogicsDirk PattinsonLutz Schröderhttps://orcid.org/0000-0002-3146-5906We 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 were explicitly stated as open in the literature.https://lmcs.episciences.org/968/pdfcomputer science - logic in computer sciencef.4.1, i.2.3 |
| spellingShingle | Dirk Pattinson Lutz Schröder Generic Modal Cut Elimination Applied to Conditional Logics Logical Methods in Computer Science computer science - logic in computer science f.4.1, i.2.3 |
| title | Generic Modal Cut Elimination Applied to Conditional Logics |
| title_full | Generic Modal Cut Elimination Applied to Conditional Logics |
| title_fullStr | Generic Modal Cut Elimination Applied to Conditional Logics |
| title_full_unstemmed | Generic Modal Cut Elimination Applied to Conditional Logics |
| title_short | Generic Modal Cut Elimination Applied to Conditional Logics |
| title_sort | generic modal cut elimination applied to conditional logics |
| topic | computer science - logic in computer science f.4.1, i.2.3 |
| url | https://lmcs.episciences.org/968/pdf |
| work_keys_str_mv | AT dirkpattinson genericmodalcuteliminationappliedtoconditionallogics AT lutzschroder genericmodalcuteliminationappliedtoconditionallogics |