SAT-based decision procedures for normal modal logics: A theoretical framework

Author(s):  
Roberto Sebastiani ◽  
Adolfo Villafiorita
2002 ◽  
Vol 16 ◽  
pp. 1-58 ◽  
Author(s):  
F. Baader ◽  
C. Lutz ◽  
H. Sturm ◽  
F. Wolter

Fusions are a simple way of combining logics. For normal modal logics, fusions have been investigated in detail. In particular, it is known that, under certain conditions, decidability transfers from the component logics to their fusion. Though description logics are closely related to modal logics, they are not necessarily normal. In addition, ABox reasoning in description logics is not covered by the results from modal logics. In this paper, we extend the decidability transfer results from normal modal logics to a large class of description logics. To cover different description logics in a uniform way, we introduce abstract description systems, which can be seen as a common generalization of description and modal logics, and show the transfer results in this general setting.


1993 ◽  
Vol 39 (1) ◽  
pp. 231-240 ◽  
Author(s):  
Claudio Cerrato

Studia Logica ◽  
2019 ◽  
Vol 108 (3) ◽  
pp. 451-476 ◽  
Author(s):  
Andrzej Pietruszczak ◽  
Mateusz Klonowski ◽  
Yaroslav Petrukhin

1999 ◽  
Vol 64 (1) ◽  
pp. 99-138 ◽  
Author(s):  
Marcus Kracht ◽  
Frank Wolter

AbstractThis paper shows that non-normal modal logics can be simulated by certain polymodal normal logics and that polymodal normal logics can be simulated by monomodal (normal) logics. Many properties of logics are shown to be reflected and preserved by such simulations. As a consequence many old and new results in modal logic can be derived in a straightforward way, sheding new light on the power of normal monomodal logic.


Sign in / Sign up

Export Citation Format

Share Document