The modal query language MDatalog

We propose a modal query language called MDatalog. A rule of an MDatalog pr ogram is a universally quantified modal Horn clause. This language is inter preted in fixed-domain first-order modal logics over signatures without fun ctions. We give algorithms to construct the least models for MDatalog progr ams. We show PTIME complexity of computing queries for a given MDatalog pro gram in the logics KD, T, KB, KDB, B, K5, KD5, K45, KD45, KB5, and S5, prov ided that the quantifier depths of queries and the program are finitely bou nded, and that the modal depth of the program is finitely bounded in the ca se when the considered logic is not an extension of K5. Some examples are g iven to illustrate application of the techniques to reason about belief and knowledge.