Logical and automated reasoning methods are crucial for web technologies and agent technologies for the intelligent processing of large ontologies, decision making based on knowledge bases of structured data, and formal specification and verification of multi-agent systems. In this joint project between the School of Computer Science at the University of Manchester and the Department of Computer Science at the University of Liverpool the aim was to use techniques from automated reasoning to develop a framework for reasoning about expressive ontology languages and expressive agent logics. The emphasis of the work at the University of Manchester was on the tableau-based reasoning for expressive ontology languages, focussing on expressive description logics and automated synthesis of tableau calculi.
In particular, we developed and implemented the first tableau decision procedure for ALBO and other expressive description logics with complex role operators including most notably role negation. This solves a long-standing open problem in the area and means that now more description logics can be solved with tableau methods. Forms of blocking are standardly used to ensure termination by limiting the number of individuals in a tableau derivation and to detect loops in the underlying models. Our approach replaces standard blocking techniques with a new blocking mechanism. This yields a stronger and more general tableau approach with which it is possible to decide non-mainstream description logics. Our method can be used in conjunction with other logics, including full first-order logic.
Building on these results we have introduced a framework for the automated synthesis of tableau calculi for description logics, modal logics and related fragments of first-order logic. The method guarantees that a generated calculus is sound and constructively complete when certain weak, natural conditions are true.
We have shown that enhancing any sound and complete tableau calculus with the unrestricted blocking mechanism produces a terminating tableau calculus, whenever the logic can be shown to admit finite filtration with respect to a well-defined first-order semantics. This is a significant result that provides on the one hand a general methodology for turning sound and constructively complete tableau calculi for modal-type logics (not only generated ones) into terminating calculi. On the other hand, it gives us a methodology for solving problems in expressive modal and description logics, for which so far it was not been known how to use tableau methods as decision procedures.
By design the tableau synthesis framework can generate tableau calculi for the description logic ALBO. The framework has also been applied to intuitionistic propositional logic and has proved useful in the ongoing EPSRC project EP/F014570/1. There we applied the method to develop the first tableau-based algorithm for checking the admissibility of global inference rules in a modal logic.
We have shown that it is possible to synthesise sound and complete tableau calculi for modal logics via another approach. This approach exploits translation to first-order logic and general principles of first-order resolution. In particular, the semantic definition of a logic is automatically transformed into clausal form and a set of inference rules. Soundness and completeness of the synthesised calculi is an immediate consequence of the soundness and completeness of the simulating resolution refinement used. The approach can be used to synthesise other deduction methods. One of the attractions of this approach is the possibility to use existing first-order resolution provers as implementations of the generated deduction calculi. Based on this work an adaptation of the first-order resolution prover SPASS has been developed in an associated MSc project by Rawan AlBarakati, which outputs modal tableau proofs and modal models.