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_s5, KDI45, KD4_s5_s, KD45_{(m)}, KD4I_g5_a, and the class of serial context-free grammar logics. We also show that MDatalog has PTIME data complexity in the logics KDI4_s5, KDI45, KD4_s5_s, and KD45_{(m)}.
Journal description