Search

Developing a good formalism and an efficient decision procedure for the instance checking problem is desirable for practical application of description logics. The data complexity of the instance checking problem is coNP-complete even for Horn knowledge bases in the basic description logic ALC. In this paper, we present and study weakenings with PTIME data complexity of the instance checking problem for Horn knowledge bases in regular description logics. We also study cases when the weakenings are an exact approximation. In contrast to previous related work of other authors, our approach deals with the case when the constructor ∀ is allowed in premises of program clauses that are used as terminological axioms. [ABSTRACT FROM AUTHOR]

We reformulate Pratt's tableau decision procedure of checking satisfiability of a set of formulas in PDL. Our formulation is simpler and its implementation is more direct. Extending the method we give the first ExpTime (optimal) tableau decision procedure not based on transformation for checking consistency of an ABox w.r.t. a TBox in PDL (here, PDL is treated as a description logic). We also prove a new result that the data complexity of the instance checking problem in PDL is coNP-complete. [ABSTRACT FROM AUTHOR]

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)}. [ABSTRACT FROM AUTHOR]

We propose a modal logic programming language called MProlog, which is as expressive as the general modal Horn fragment. We give a fixpoint semantics and an SLD-resolution calculus for MProlog in all of the basic serial modal logics KD, T, KDB, B, KD4, S4, KD5, KD45, and S5. For an MProlog program P and for L being one of the mentioned logics, we define an operator T_{L,P}, which has the least fixpoint I_{L,P}. This fixpoint is a set of formulae, which may contain labeled forms of the modal operator ⋄, and is called the least L-model generator of P. The standard model of I_{L,P} is shown to be a least L-model of P. The SLD-resolution calculus for MProlog is designed with a similar style as for classical logic programming. It is sound and complete. We also extend the calculus for MProlog in the almost serial modal logics KB, K5, K45, and KB5. [ABSTRACT FROM AUTHOR]

Provides information on MDatalog, a modal query language. Basic definitions for propositional modal logics; Definition of fixed-domain first-order modal logics over signatures without functions; Order between first-order Kripke models; Discussion on the implementation of algorithms for constructing the least models for MDatalog programs.