Foundations of Modal Deductive Databases

We give formulations for modal deductive databases and present a modal query language called MDatalog. We define modal relational algebras and give the seminaive evaluation algorithm, the top-down evaluation algorithm, and the magic-set transformation for MDatalog queries. The results of this paper like soundness and completeness of the top-down evaluation algorithm or correctness of the magic-set transformation are proved for the multimodal logics of belief KDI4 _s 5, KDI45, KD4 _s 5 _s , KD45 _{(m)} , KD4I _g 5 _a , and the class of serial context-free grammar logics. We also show that MDatalog has PTIME data complexity in the logics KDI4 _s 5, KDI45, KD4 _s 5 _s , and KD45 _{(m)} .