Name
Abstract | ||
|---|---|---|
This paper studies Gentzen-style sequent calculi for multi-modal logics with interaction between the modalities. We prove cut elimination and some of its usual corollaries for two such logics: Standard Deontic Logic with the Ought-implies-Can principle, and a non-normal deontic logic where obligation, permissions and abilities interact in a complex way. The key insight of these results is to make rules sensitive to the shape of the formulas on either sides of the sequents. This way one can devise rules in a much more modular fashion. This feature of Hilbert-style systems is notoriously lost when one moves to sequent calculi. By partly restoring modularity the method proposed here can potentially provide a unified approach to the proof theory of multi-modal systems. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1007/978-3-642-40948-6_10 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Deontic logic,Sequent calculus,Substructural logic,Proof theory,Sequent,Artificial intelligence,Modal logic,Dynamic logic (digital electronics),Calculus,Modularity,Mathematics | Conference | 8196 |
ISSN | Citations | PageRank |
0302-9743 | 4 | 0.57 |
References | Authors | |
12 | 1 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Norbert Gratzl | 1 | 10 | 3.89 |