Practical Reasoning Approaches for Web Ontologies and Multi-Agent Systems


EPSRC Research Project EP/D056152/1
Principal Investigator:
Dr Renate Schmidt
Research Associate:
Dr Dmitry Tishkovsky
Start Date:
15/01/2007
End Date:
14/01/2010
Collaborating Project:
EPSRC EP/D060451/1, University of Liverpool

Summary

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.

Software

Bibliography

1
R. G. AlBarakati.
Development of a tableaux resolution prover.
Master's thesis, The University of Manchester, UK, 2009.

2
D. M. Gabbay, R. A. Schmidt, and A. Szaas.
Second-Order Quantifier Elimination: Foundations, Computational Aspects and Applications, volume 12 of Studies in Logic: Mathematical Logic and Foundations.
College Publications, 2008.

3
I. Horrocks, U. Hustadt, U. Sattler, and R. A. Schmidt.
Computational modal logic.
In P. Blackburn, J. van Benthem, and F. Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in Logic and Practical Reasoning, pages 181-245. Elsevier, Amsterdam, 2007.
Commissioned overview paper.

4
R. A. Schmidt.
Improved second-order quantifier elimination in modal logic.
In S. Hölldobler, C. Lutz, and H. Wansing, editors, Proceedings of the 11th European Conference on Logics in Artificial Intelligence (JELIA), volume 5293 of Lecture Notes in Artificial Intelligence, pages 375-388. Springer, 2008.

5
R. A. Schmidt.
A new methodology for developing deduction methods.
Annals of Mathematics and Artificial Intelligence, 55(1-2):155-187, 2009.

6
R. A. Schmidt and U. Hustadt.
The axiomatic translation principle for modal logic.
ACM Transactions on Computational Logic, 8(4):1-55, 2007.

7
R. A. Schmidt and D. Tishkovsky.
Using tableau to decide expressive description logics with role negation.
In K. Aberer, K.-S. Choi, N. Fridman Noy, D. Allemang, K.-I. Lee, L. J. B. Nixon, J. Golbeck, P. Mika, D. Maynard, R. Mizoguchi, G. Schreiber, and P. Cudré-Mauroux, editors, The Semantic Web, 6th International Semantic Web Conference, 2nd Asian Semantic Web Conference, ISWC 2007 + ASWC 2007, Busan, Korea, November 11-15, 2007, volume 4825 of Lecture Notes in Computer Science, pages 438-451. Springer, 2007.

8
R. A. Schmidt and D. Tishkovsky.
A general tableau method for deciding description logics, modal logics and related first-order fragments.
In A. Armando, P. Baumgartner, and G. Dowek, editors, Automated Reasoning (IJCAR 2008), volume 5195 of Lecture Notes in Computer Science, pages 194-209. Springer, 2008.

9
R. A. Schmidt and D. Tishkovsky.
On combinations of propositional dynamic logic and doxastic modal logics.
Journal of Logic, Language and Information, 17(1):109-129, 2008.

10
R. A. Schmidt and D. Tishkovsky.
Automated synthesis of tableau calculi.
In M. Giese and A. Waaler, editors, Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2009), volume 5607 of Lecture Notes in Computer Science, pages 310-324. Springer, 2009.

11
C. Weidenbach, R. A. Schmidt, T. Hillenbrand, R. Rusev, and D. Topic.
System description: SPASS version 3.0.
In F. Pfenning, editor, Automated Deduction--CADE-21, volume 4603 of Lecture Notes in Artificial Intelligence, pages 514-520. Springer, 2007.


Last modified: 11 Mar 10
Copyright © 2010 Renate A. Schmidt, School of Computer Science, Univ. Man., schmidt@cs.man.ac.uk