Abstract
We consider multi-modal logic Kw(with countably infinite number of basic modalities) extended with additional modalities ∪ and ∩ corresponding to the union and intersection of all basic modalities. We present complete and sound axiomatic systems and polynomial-space terminating tableau-based decision procedures for the basic logic in this language, and its deterministic counterpart. We also show that admits filtration, which can be used independently of our tableaux to establish its decidability.
Original language | English |
---|---|
Pages (from-to) | 275-294 |
Number of pages | 20 |
Journal | Journal of Applied Non-Classical Logics |
Volume | 22 |
Issue number | 4 |
DOIs | |
Publication status | Published - 1 Dec 2012 |
Externally published | Yes |
Keywords
- axiomatic systems
- filtration
- infinite intersections and unions
- modal logic
- tableau-based decision procedures