From Tableaux to Automata for Description Logics

• Autorzy: Baader F. , Hladik J. , Lutz C. , Wolter F.
• Języki publikacji: EN

Abstrakty

EN

This paper investigates the relationship between automata- and tableau-based inference procedures for description logics. To be more precise, we develop an abstract notion of what a tableau-based algorithm is, and then show, on this abstract level, how tableau-based algorithms can be converted into automata-based algorithms. In particular, this allows us to characterize a large class of tableau-based algorithms that imply an ExpTime upper-bound for reasoning in the description logics for which such an algorithm exists.

Słowa kluczowe

EN

description logics; tableau algorithms; ExpTime-admissible

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2003
• Tom: Vol. 57, nr 2-4
• Strony: 247--279
• Opis fizyczny: Bibliogr. 38 poz.

Twórcy

autor

Baader F.

• Theoretical Computer Science, TU Dresden, D-01062 Dresden, Germany

autor

Hladik J.

• Theoretical Computer Science, TU Dresden, D-01062 Dresden, Germany

autor

Lutz C.

• Theoretical Computer Science, TU Dresden, D-01062 Dresden, Germany

autor

Wolter F.

• Department of Computer Science, University of Liverpool Liverpool L69 7ZF, U.K.

Bibliografia

• [1] F. Baader, D. Calvanese, D. McGuinness, D. Nardi, and P. F. Patel-Schneider, editors. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press, 2003.
• [2] F. Baader, E. Franconi, B. Hollunder, B. Nebel, and H.-J. Profitlich. An empirical analysis of optimization techniques for terminological representation systems or: Making KRIS get a move on. Applied Artificial Intelligence. Special Issue on Knowledge Base Management, 4:109-132, 1994.
• [3] F. Baader, J. Hladik, C. Lutz, and F. Wolter. From tableaux to automata for description logics. In M. Vardi and A. Voronkov, editors, Proceedings of the 10th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2003), volume 2850 of Lecture Notes in Computer Science, pages 1-32, Almaty, Kazakhstan, 2003. Springer-Verlag.
• [4] F. Baader and W. Nutt. Basic description logics. In [1], pages 43-95. 2003.
• [5] F. Baader and U. Sattler. An overview of tableau algorithms for description logics. Studia Logica, 69:5-40, 2001.
• [6] F. Baader and S. Tobies. The inverse method implements the automata approach for modal satisfiability. In Proc. of the Int. Joint Conf. on Automated Reasoning IJCAR’01, volume 2083 of LNAI, pages 92-106. Springer-Verlag, 2001.
• [7] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001.
• [8] R. J. Brachman and H. J. Levesque, editors. Readings in Knowledge Representation. Morgan Kaufmann, Los Altos, 1985.
• [9] D. Calvanese and G. DeGiacomo. Expressive description logics. In [1], pages 178-218. 2003.
• [10] G. De Giacomo and M. Lenzerini. TBox and ABox reasoning in expressive description logics. In L. C. Aiello, J. Doyle, and S. C. Shapiro, editors, Proc. of the 5th Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR’96), pages 316-327.Morgan Kaufmann, Los Altos, 1996.
• [11] F. Donini. Complexity of reasoning. In [1], pages 96-136. 2003.
• [12] F. Donini and F. Massacci. EXPTIME tableaux for ALC. Acta Informatica, 124(1):87-138, 2000.
• [13] F. M. Donini, M. Lenzerini, D. Nardi, and W. Nutt. The complexity of concept languages. In J. Allen, R. Fikes, and E. Sandewall, editors, Proc. of the 2nd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR’91), pages 151-162.Morgan Kaufmann, Los Altos, 1991.
• [14] F. M. Donini, M. Lenzerini, D. Nardi, and W. Nutt. Tractable concept languages. In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI’91), pages 458-463, Sydney (Australia), 1991.
• [15] V. Haarslev and R. Möller. RACER system description. In Proc. of the Int. Joint Conf. on Automated Reasoning (IJCAR 2001), 2001.
• [16] B. Hollunder and F. Baader. Qualifying number restrictions in concept languages. In Proc. of the 2nd Int. Conf. on the Principles of Knowledge Representation and Reasoning (KR’91), pages 335-346, 1991.
• [17] I. Horrocks. Using an expressive description logic: FaCT or fiction? In Proc. of the 6th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR’98), pages 636-647, 1998.
• [18] I. Horrocks. Implementation and optimization techniques. In [1], pages 306-346. 2003.
• [19] I. Horrocks and U. Sattler. A description logic with transitive and inverse roles and role hierarchies. J. of Logic and Computation, 9(3):385-410, 1999.
• [20] I. Horrocks, U. Sattler, and S. Tobies. Practical reasoning for expressive description logics. In H. Ganzinger, D. McAllester, and A. Voronkov, editors, Proc. of the 6th Int. Conf. on Logic for Programming and Automated Reasoning (LPAR’99), number 1705 in Lecture Notes in Artificial Intelligence, pages 161-180. Springer-Verlag, 1999.
• [21] I. Horrocks, U. Sattler, and S. Tobies. Practical reasoning for very expressive description logics. J. of the Interest Group in Pure and Applied Logic, 8(3):239-264, 2000.
• [22] R. Kontchakov, C. Lutz, F. Wolter, and M. Zakharyaschev. Temporal tableaux. Studia Logica, 2003. To appear.
• [23] R. MacGregor. The evolving technology of classification-based knowledge representation systems. In J. F. Sowa, editor, Principles of Semantic Networks, pages 385-400.Morgan Kaufmann, Los Altos, 1991.
• [24] E. Mays, R. Dionne, and R. Weida. K-REP system overview. SIGART Bull., 2(3), 1991.
• [25] M. Minsky. A framework for representing knowledge. In J. Haugeland, editor, Mind Design. The MIT Press, 1981. A longer version appeared in The Psychology of Computer Vision (1975). Republished in [8].
• [26] R. Möller and V. Haarslev. Description logic systems. In [1], pages 282-305. 2003.
• [27] G. Pan, U. Sattler, and M. Y. Vardi. BDD-based decision procedures for K. In A. Voronkov, editor, Proc. of the 18th Int. Conf. on Automated Deduction (CADE 2002), volume 2392 of LNAI, pages 16-30. Springer-Verlag, 2002.
• [28] G. Pan and M. Y. Vardi. Optimizing a bdd-based modal solver. In F. Baader, editor, Proc. of the 19th Int. Conf. on Automated Deduction (CADE 2003), volume 2741 of LNAI, pages 75-89. Springer-Verlag, 2003.
• [29] P. F. Patel-Schneider, D. L. McGuiness, R. J. Brachman, L. Alperin Resnick, and A. Borgida. The CLASSIC knowledge representation system: Guiding principles and implementation rational. SIGART Bull., 2(3):108-113, 1991.
• [30] C. Peltason. The BACK system—an overview. SIGART Bull., 2(3):114-119, 1991.
• [31] M. R. Quillian. Word concepts: A theory and simulation of some basic capabilities. Behavioral Science, 12:410-430, 1967. Republished in [8].
• [32] K. Schild. A correspondence theory for terminological logics: Preliminary report. In Proc. of the 12th Int. Joint Conf. on Artificial Intelligence (IJCAI’91), pages 466-471, 1991.
• [33] M. Schmidt-Schauß and G. Smolka. Attributive concept descriptions with complements. Artificial Intelligence, 48(1):1-26, 1991.
• [34] E. Spaan. Complexity of Modal Logics. PhD thesis, Department of Mathematics and Computer Science, University of Amsterdam, 1993.
• [35] S. Tobies. A PSPACE algorithm for graded modal logic. In H. Ganzinger, editor, Proc. of the 16th Int. Conf. on Automated Deduction (CADE’99), volume 1632 of Lecture Notes in Artificial Intelligence, pages 52-66. Springer-Verlag, 1999.
• [36] M. Y. Vardi and P. Wolper. Automata-theoretic techniques for modal logics of programs. J. of Computer and System Sciences, 32:183-221, 1986. A preliminary version appeared in Proc. of the 16th ACM SIGACT Symp. on Theory of Computing (STOC’84).
• [37] A. Voronkov. How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi. ACM Trans. on Comp. Logic, 2(2):182-215, 2001.
• [38] W. A. Woods and J. G. Schmolze. The KL-ONE family. In F. W. Lehmann, editor, Semantic Networks in Artificial Intelligence, pages 133-178. Pergamon Press, 1992. Published as a special issue of Computers & Mathematics with Applications, Volume 23, Number 2-9.