A relational dual tableau decision procedure for multimodal and description logics

Abstract

We present a dual tableau based decision procedure for a class of fragments of the classical relational logic of binary relations. The logics considered share a common language involving a restricted composition operator and infinitely many relational constants which may have the properties of reflexivity, transitivity, and heredity. The construction of the dual tableau is carried out by applying in a deterministic way axioms and inference rules of the system without resorting to external tools. An important feature of the dual tableau procedure is a rule to handle the relational composition operator, that permits to decompose in a single step compositional formulae and negative compositional formulae with the same left object variable. Our relational dual tableau can be used as a decision procedure for validity verification in the multimodal logic K, the description logic ALC, and several non-classical logics for reasoning in various AI systems. © 2014 Springer International Publishing.