A modal logic formalism for efficient knowledge representation and reasoning

Modal and modal-like logics have become the focus of rcriewed attentiorl in the field of knowledge representation and automated reasoning. They provide a good middle-ground between expressiveness and complexity, which makes them suitable candidates for representation of ontologies on the Semantic Web. Expressive modal logics are well-known to be decidable but intractable. This problem has been addressed mostly by optimizations to improve the efficiency of reasoners on top of existing formalisms and algorithms, which have largely been unchanged since the days of Kripke. This work addresses the problem of intractability by providing an improved definition of models. Rather than on a per-world basis as in Kripke models, truth assignments are specified over set of worlds addressed by labels with variables. The set of worlds represented by a label is the set of all its ground instances. This allows satisfying models to be stored in a more compact form. We prove that our representation of models and formulas preserves the satisfiability of formulas. Our model-finding algorithm can be understood as an extension of nogood reasoning for propmitiornal logic, whcrcits the nogoods are pararrietrized by labels, i.e. sets of worlds in which they apply. Nogoods ensure termination of the algorithm. The search strategy is general enough to accommodate tableau-style or DPLL-style branching. The algorithm is specified in sufficient detail so as to make it readily implementable, although we do not actually provide an implementation. For simplicity, we describe our theory only on the modal logic K. An adaptation to multimodal logics, the description logic ACC, Quantified Boolean Formulas, and Propositional Dynamic Logic is straightforward; we also outline how the approach extends to logics with global axioms, such as reflexivity, transitivity, symmetry etc. We also outline the connection with recent advances of tableau- arid DPLL-style n~ethods in first-order logic.