An Efficient Tableau Prover using Global Caching for the Description Logic ALC

• Autorzy: Nguyen L.A. L.A.
• Języki publikacji: EN

Abstrakty

EN

We report on our implementation of a tableau prover for the description logic ALC, which is based on the EXPTIME tableau algorithm using global caching for ALC that was developed jointly by us and Gor´e [9]. The prover, called TGC for "Tableaux with Global Caching", checks satisfiability of a set of concepts w.r.t. a set of global assumptions by constructing an and-or graph, using tableau rules for expanding nodes. We have implemented for TGC a special set of optimizations which co-operates very well with global caching and various search strategies. The test results on the test set T98-sat of DL'98 Systems Comparison indicate that TGC is an efficient prover for ALC. This suggests that global caching together with the set of optimizations used for TGC is worth implementing and experimenting also for other modal/description logics.

Słowa kluczowe

EN

automated reasoning; tableaux; description logics; global caching; optimization

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 93, nr 1-3
• Strony: 273--288
• Opis fizyczny: Bibliogr. 23 poz., tab.

Twórcy

autor

Nguyen L.A. L.A.

• Institute of Informatics University of Warsaw Banacha 2, 02-097 Warsaw, Poland,

Bibliografia

• [1] F. Baader, M. Buchheit, and B. Hollunder. Cardinality restrictions on concepts. Artif. Intell., 88(1-2):195-213, 1996.
• [2] F. Baader and U. Sattler. An overview of tableau algorithms for description logics. Studia Logica, 69:5-40, 2001.
• [3] P. Balsiger and A. Heuerding. Comparison of theorem provers for modal logics - introduction and summary. In H.C.M. de Swart, editor, Proceedings of TABLEAUX'1998, LNCS 1397, pages 25-26. Springer, 1998.
• [4] Y. Ding and V. Haarslev. Tableau caching for description logics with inverse and transitive roles. In Proc. DL-2006: International Workshop on Description Logics, pages 143-149, 2006.
• [5] F. Donini and F. Massacci. EXPTime tableaux for ALC. Artificial Intelligence, 124:87-138, 2000.
• [6] M. Fitting. Proof Methods for Modal and Intuitionistic Logics. volume 169 of Synthese Library. D. Reidel, Dordrecht, Holland, 1983.
• [7] R. Goré. Tableau methods for modal and temporal logics. In D'Agostino et al, editor, Handbook of Tableau Methods, pages 297-396. Kluwer, 1999.
• [8] R. Goré and L.A. Nguyen. A tableau system with automaton-labelled formulae for regular grammar logics. In B. Beckert, editor, Proceedings of TABLEAUX 2005, LNAI 3702, pages 138-152. Springer-Verlag, 2005.
• [9] R. Goré and L.A. Nguyen. EXPTIME tableaux for ALC using sound global caching. In D. Calvanese et al., editor, Proceedings of Description Logics 2007, pages 299-306, 2007.
• [10] R. Goré and L.A. Nguyen. EXPTIME tableaux with global caching for description logics with transitive roles, inverse roles and role hierarchies. In N. Olivetti, editor, Proc. of TABLEAUX 2007, LNAI 4548, pages 133-148. Springer-Verlag, 2007.
• [11] R. Goré and L.A. Nguyen. Optimised EXPTIME tableaux for ALC using sound global caching, propagation and cutoffs. Manuscript, available at http://www.mimuw.edu.pl/~nguyen/papers.html, 2007.
• [12] R. Goré and L.A. Nguyen. Analytic cut-free tableaux for regular modal logics of agent beliefs. In F. Sadri and K. Satoh, editors, Proceedings of CLIMA VIII, LNAI 5056, pages 268-287. Springer-Verlag, 2008.
• [13] R. Goré and L.A. Nguyen. Sound global caching for abstract modal tableaux. In H.-D. Burkhard, G. Lindemann, and H. Schlingloff, editors, Proceedings of CS&P'2008, pages 157-167, 2008.
• [14] V. Haarslav and R. Mőller. Consistency testing: The RACE experience. In R. Dyckhoff, editor, TABLEAUX- 2000: Proceedings of the International Conference on Theorem Proving with Analytic Tableaux and Related Methods, volume LNCS 1847, pages 57-61. Springer, 2000.
• [15] I. Horrocks and P.F. Patel-Schneider. Optimizing description logic subsumption. J. Log. Comput., 9(3):267-293, 1999.
• [16] I. Horrocks and U. Sattler. A description logic with transitive and inverse roles and role hierarchies. J. Log. Comput., 9(3):385-410, 1999.
• [17] I. Horrocks, U. Sattler, and S. Tobies. Reasoning with individuals for the description logic SHIQ. In D.A. McAllester, editor, Proceedings of CADE-17, LNCS 1831, pages 482-496. Springer, 2000.
• [18] C. Lutz. Complexity of terminological reasoning revisited. In H. Ganzinger, D.A. McAllester, and A. Voronkov, editors, Proceedings of LPAR'1999, LNCS 1705, pages 181-200. Springer, 1999.
• [19] B. Motik, R. Shearer, and I. Horrocks. Optimized reasoning in description logics using hypertableaux. In F. Pfenning, editor, Proceedings of CADE-21, LNCS 4603, pages 67-83, 2007.
• [20] L.A. Nguyen. The long version of this paper. Available at http://www.mimuw.edu.pl/~nguyen/papers.html, 2008.
• [21] L.A. Nguyen. The source code of TGC. Available at http://www.mimuw.edu.pl/~nguyen/systems.html, 2008.
• [22] K. Schild. Terminological cycles and the propositional μ-calculus. In J. Doyle, E. Sandewall, and P. Torasso, editors, Proceedings of KR'94, LNCS 4130, pages 509-520.Morgan Kaufmann, 1994.
• [23] D. Tsarkov and I. Horrocks. Description logic reasoner: System description. In U. Furbach and N. Shankar, editors, Proceedings of IJCAR'2006, pages 292-297. Springer, 2006.