×

EXPtime tableaux for ALC. (English) Zbl 0952.68136

The last years have seen two major advances in knowledge representation and reasoning. First, many interesting problems (ranging from semi-structured data to linguistics) were shown to be expressible in logics whose main deductive problems are EXPtime-complete. Second, experiments in automated reasoning have substantially broadened the meaning of “practical tractability”. Instances of realistic size for Pspace-complete problems are now within reach for implemented systems. Still, there is a gap between the reasoning services needed by the expressive logics mentioned above and those provided by the current systems. Indeed, the algorithms based on tree-automata, which are used to prove EXPtime-completeness, require exponential time and space even in simple cases. On the other hand, current algorithms based on tableau methods can take advantage of such cases, but require double exponential time in the worst case. We propose a tableau calculus for the description logic \(ALC\) for checking the satisfiability of a concept with respect to a TBox with general axioms, and transform it into the first simple tableau-based decision procedure working in single exponential time. To guarantee the ease of implementation, we also discuss the effects that optimizations (propositional backjumping, simplification, semantic branching, etc.) might have on our complexity result, and introduce a few optimizations ourselves.

MSC:

68T30 Knowledge representation

Software:

HARP; LEDA
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abadi, M.; Burrows, M.; Lampson, B.; Plotkin, G. D., A calculus for access control in distributed systems, ACM Trans. Program. Lang. Syst., Vol. 15, 4, 706-734 (1993)
[2] Arai, N., A proper hierarchy of propositional sequent calculi, Theoret. Comput. Sci., Vol. 159, 2, 343-354 (1996) · Zbl 0871.68161
[3] Baader, F.; Hollunder, B.; Nebel, B.; Profitlich, H.-J.; Franconi, E., An empirical analysis of optimization techniques for terminological representation systems or: “making KRIS get a move on”, Appl. Intelligence, Vol. 4, 2, 109-132 (1994)
[4] Basin, D.; Matthews, S.; Vigano, L., A new method for bounding the complexity of modal logics, (Gottlob, G.; Leitsch, A.; Mundici, D., Proc. 5th Kurt Gödel Colloquium, KGC’97. Proc. 5th Kurt Gödel Colloquium, KGC’97, Lecture Notes in Computer Science, Vol. 1289 (1997), Springer: Springer Berlin), 89-102 · Zbl 0886.03039
[5] Baumgartner, P.; Furbach, U.; Niemelä, I., Hyper tableaux, (Alferes, J.; Pereira, L.; Orlowska, E., Proc. 5th European Workshop on Logics in Artificial Intelligence (JELIA’96). Proc. 5th European Workshop on Logics in Artificial Intelligence (JELIA’96), Lecture Notes in Artificial Intelligence, Vol. 1126 (1996), Springer: Springer Berlin), 1-17 · Zbl 1427.03031
[6] Blackburn, P.; Spaan, E., A modal perspective on computational complexity of attribute value grammar, J. Logic Language and Inform., Vol. 2, 129-169 (1993) · Zbl 0793.03018
[7] Borgida, A.; Patel-Schneider, P., A semantics and complete algorithm for subsumption in the CLASSIC description logic, J. Artificial Intelligence Res., Vol. 1, 277-308 (1994) · Zbl 0900.68397
[8] Buchheit, M.; Donini, F. M.; Schaerf, A., Decidable reasoning in terminological knowledge representation systems, J. Artificial Intelligence Res., Vol. 1, 109-138 (1993) · Zbl 0900.68396
[9] Calvanese, D.; De Giacomo, G.; Lenzerini, M., What can knowledge representation do for semi-structured data?, (Proc. AAAI-98, Madison, WI (1998)), 205-210
[10] Calvanese, D.; De Giacomo, G.; Lenzerini, M.; Nardi, D.; Rosati, R., Description logic framework for information integration, (Proc. 6th International Conference on Principles of Knowledge Representation and Reasoning (KR-98), Trento, Italy (1998)), 2-13
[11] Castilho, M.; Fariñas del Cerro, L.; Gasquet, O.; Herzig, A., Modal tableaux with propagation rules and structural rules, Fundamenta Informaticae, Vol. 32, 3, 281-297 (1997) · Zbl 0926.03020
[12] Cerrito, S.; Cialdea Myer, M., Hintikka multiplicities in matrix decision methods for some propositional modal logics, (Galmiche, D., Proc. International Conference on Analytic Tableaux and Related Methods (TABLEAUX’97). Proc. International Conference on Analytic Tableaux and Related Methods (TABLEAUX’97), Lecture Notes in Artificial Intelligence, Vol. 1227 (1997), Springer: Springer Berlin), 138-152 · Zbl 1415.03035
[13] Courcoubetis, C.; Vardi, M.; Wolper, P.; Yannakakis, M., Memory efficient algorithms for the verification of temporal properties, Formal Methods in System Design, Vol. 1, 275-288 (1992)
[14] De Giacomo, G.; Lenzerini, M., Tbox and abox reasoning in expressive description logics, (Proc. 5th International Conference on the Principles of Knowledge Representation and Reasoning (KR-96), Cambridge, MA (1996), Morgan Kaufmann: Morgan Kaufmann Los Altos, CA), 316-327
[15] De Giacomo, G.; Lenzerini, M., A uniform framework for concept definitions in description logics, J. Artificial Intelligence Res., Vol. 6, 87-110 (1997) · Zbl 0894.68095
[16] G. De Giacomo, F. Massacci, Combining deduction and model checking into tableaux and algorithms for Converse-PDL, to appear in Information and Computation (accepted in 1997). An online version is at http://www.academicpress.com/i&c on IDEALfirst. A preliminary version appeared in: Proc. CADE-96, Lecture Notes in Artificial Intelligence, Vol. 1104, 1996, Springer, Berlin, pp. 613-628; G. De Giacomo, F. Massacci, Combining deduction and model checking into tableaux and algorithms for Converse-PDL, to appear in Information and Computation (accepted in 1997). An online version is at http://www.academicpress.com/i&c on IDEALfirst. A preliminary version appeared in: Proc. CADE-96, Lecture Notes in Artificial Intelligence, Vol. 1104, 1996, Springer, Berlin, pp. 613-628
[17] Dechter, R., Enhancement schemes for constraint processing: Backjumping, learning, and cutset decomposition, Artificial Intelligence, Vol. 41, 3, 273-312 (1990)
[18] Demri, S., Uniform and non uniform strategies for tableaux calculi for modal logics, J. Appl. Non-Classical Logics, Vol. 5, 1, 77-96 (1995) · Zbl 0826.03006
[19] Devambu, P.; Brachman, R. J.; Selfridge, P. J.; Ballard, B. W., LASSIE: A knowledge-based software information system, Comm. ACM, Vol. 34, 5, 36-49 (1991)
[20] Donini, F. M.; De Giacomo, G.; Massacci, F., EXPTIME tableaux for \(ALC\), (Padgham, L.; Franconi, E.; Gehrke, M.; McGuinness, D.; Patel-Schneider, P., Proc. 1996 Description Logic Workshop (DL-96). Proc. 1996 Description Logic Workshop (DL-96), no. WS-96-05 in AAAI Technical Reports Series (1996), AAAI Press/MIT Press), 107-110 · Zbl 0952.68136
[21] Donini, F. M.; Lenzerini, M.; Nardi, D.; Nutt, W., Tractable concept languages, (Proc. IJCAI-91, Sydney, Australia (1991)), 458-463 · Zbl 0742.68066
[22] Donini, F. M.; Lenzerini, M.; Nardi, D.; Nutt, W., The complexity of concept languages, Inform. and Comput., Vol. 134, 1-58 (1997) · Zbl 0906.68145
[23] Doyle, J.; Patil, R., Two theses of knowledge representation: Language restrictions, taxonomic classification, and the utility of representation services, Artificial Intelligence, Vol. 48, 261-297 (1991)
[24] Emerson, A. E., Automated temporal reasoning about reactive systems, (Moller, F.; Birtwistle, G., Logics for Concurrency (Structure versus Automata). Logics for Concurrency (Structure versus Automata), Lecture Notes in Computer Science, Vol. 1043 (1996), Springer: Springer Berlin), 41-101
[25] Fagin, R.; Halpern, J. Y.; Moses, Y.; Vardi, M. Y., Reasoning about Knowledge (1995), MIT Press: MIT Press Cambridge, MA · Zbl 0839.68095
[26] Fariñas del Cerro, L.; Gasquet, O., Tableaux based decision procedures for modal logics of confluence and density, Fundamenta Informaticae, Vol. 40, 4, 317-333 (1999) · Zbl 0942.03009
[27] Fischer, N. J.; Ladner, R. E., Propositional dynamic logic of regular programs, J. Comput. System Sci., Vol. 18, 194-211 (1979) · Zbl 0408.03014
[28] Fitting, M., Proof Methods for Modal and Intuitionistic Logics (1983), Reidel: Reidel Dordrecht · Zbl 0523.03013
[29] Fitting, M., Basic modal logic, (Gabbay, D.; Hogger, C.; Robinson, J., Handbook of Logic in Artificial Intelligence and Logic Programming, Vol. 1 (1993), Oxford University Press: Oxford University Press Oxford), 365-448
[30] (Franconi, E.; etal., Proc. 1998 Internat. Workshop on Description Logics. Proc. 1998 Internat. Workshop on Description Logics, Technical Report ITC-IRST 9805-03 (1998)), Available as CEUR Publication at http://SunSite.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/Vol-11/
[31] Gerth, R.; Peled, D.; Vardi, M.; Wolper, P., Simple on-the-fly automatic verification of linear temporal logic, (Protocol Specification Testing and Verification (PSVT-95), Warsaw, Poland (1995), Chapman Hall), 3-18
[32] Giunchiglia, E.; Giunchiglia, F.; Sebastiani, R.; Tacchella, A., SAT vs. translation based decision procedures for modal logics: A comparative evaluation, J. Appl. Non-Classical Logics, Vol. 10, 2 (2000) · Zbl 1033.03500
[33] Giunchiglia, E.; Tacchella, A., A subset-matching size-bounded cache for satisfiability in modal logics, (Dyckhoff, R., Proc. 4th International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2000). Proc. 4th International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2000), Lecture Notes in Artificial Intelligence, Vol. 1847 (2000), Springer: Springer Berlin) · Zbl 0963.68178
[34] Giunchiglia, F.; Sebastiani, R., Building decision procedures for modal logics from propositional decision procedures—The case study of modal K, (McRobbie, M. A.; Slaney, J. K., Proc. 13th International Conference on Automated Deduction (CADE’96). Proc. 13th International Conference on Automated Deduction (CADE’96), Lecture Notes in Artificial Intelligence, Vol. 1104 (1996), Springer: Springer Berlin), 583-597 · Zbl 1415.03022
[35] Glasgow, J.; MacEwen, G.; Panangaden, P., A logic for reasoning about security, ACM Trans. Comput. Syst., Vol. 10, 3, 226-264 (1992)
[36] Goré, R., Tableau methods for modal and temporal logics, (D’Agostino, M.; Gabbay, D.; Hähnle, R., Handbook of Tableau Methods (1999), Kluwer Academic: Kluwer Academic Dordrecht) · Zbl 0972.03529
[37] Haarslev, V.; Möller, R., Consistency testing: The RACE experience, (Dyckhoff, R., Proc. 4th International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2000). Proc. 4th International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2000), Lecture Notes in Artificial Intelligence, Vol. 1847 (2000), Springer: Springer Berlin) · Zbl 0963.68517
[38] Halpern, J. Y.; Moses, Y., A guide to completeness and complexity for modal logics of knowledge and belief, Artificial Intelligence, Vol. 54, 319-379 (1992) · Zbl 0762.68029
[39] Heuerding, A.; Seyfried, M.; Zimmermann, H., Efficient loop-check for backward proof search in some non-classical logics, (Proc. 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX’96). Proc. 5th Workshop on Theorem Proving with Analytic Tableaux and Related Methods (TABLEAUX’96), Lecture Notes in Artificial Intelligence, Vol. 1071 (1996), Springer: Springer Berlin), 210-225 · Zbl 1415.03023
[40] Hoffman, J.; Koehler, J., A new method to index and query sets, (Proc. IJCAI-99, Stockholm, Sweden (1999), Morgan Kaufmann: Morgan Kaufmann Los Altos, CA), 462-467
[41] Horrocks, I., Using an expressive description logic: FaCT or fiction?, (Proc. 6th International Conference on Principles of Knowledge Representation and Reasoning (KR-98), Trento, Italy (1998), Morgan Kaufmann: Morgan Kaufmann Los Altos, CA), 636-647
[42] Horrocks, I., Benchmark analysis with FaCT, (Dyckhoff, R., Proc. 4th International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2000). Proc. 4th International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2000), Lecture Notes in Artificial Intelligence, Vol. 1847 (2000), Springer: Springer Berlin), 62-66 · Zbl 0963.68516
[43] Horrocks, I.; Patel-Schneider, P. F., Optimizing description logic subsumption, J. Logic Comput., Vol. 9, 3, 267-293 (1999) · Zbl 0940.03038
[44] Horrocks, I.; Sattler, U., A description logic with transitive and inverse roles and role hierarchies, J. Logic Comput., Vol. 9, 3, 385-410 (1999) · Zbl 0940.03039
[45] Horrocks, I.; Sattler, U.; Tobies, S., Practical reasoning for expressive description logics, J. Interest Group in Pure and Applied Logic, Vol. 8, 3, 239-263 (2000) · Zbl 0967.03026
[46] Horrocks, I.; Tobies, S., Reasoning with axioms: Theory and practice, (Cohen, A. G.F.; Selman, B., Proc. 7th International Conference on Principles of Knowledge Representation and Reasoning (KR’2000), Breckenridge, CO (2000), Morgan Kaufmann: Morgan Kaufmann Los Altos, CA), 285-296
[47] Hustadt, U.; Schmidt, R. A., On the relation of resolution and tableaux proof systems for description logics, (Dean, T., Proc. IJCAI-99, Stockholm, Sweden (1999), Morgan Kaufmann: Morgan Kaufmann Los Altos, CA), 110-115
[48] Hustadt, U.; Schmidt, R. A., An empirical analysis of modal theorem provers, J. Appl. Non-Classical Logics, Vol. 9, 4, 479-522 (1999) · Zbl 1033.03501
[49] Kozen, D.; Tiuryn, J., Logic of programs, (van Leeuwen, J., Handbook of Theoretical Computer Science, Vol. II (1990), Elsevier Science (North-Holland): Elsevier Science (North-Holland) Amsterdam), Chapter 14, pp. 789-840 · Zbl 0900.68306
[50] Kripke, S., Semantical analysis of modal logic I: Normal propositional calculi, Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik, Vol. 9, 67-96 (1963) · Zbl 0118.01305
[51] Ladner, R. E., The computational complexity of provability in systems of modal propositional logic, SIAM J. Comput., Vol. 6, 3, 467-480 (1977) · Zbl 0373.02025
[52] Levesque, H. J., Foundations of a functional approach to knowledge representation, Artificial Intelligence, Vol. 23, 155-212 (1984) · Zbl 0548.68090
[53] Levesque, H. J.; Brachman, R. J., A fundamental tradeoff in knowledge representation and reasoning, (Brachman, R. J.; Levesque, H. J., Readings in Knowledge Representation (1985), Morgan Kaufmann: Morgan Kaufmann Los Altos, CA), 41-70
[54] Massacci, F., Strongly analytic tableaux for normal modal logics, (Bundy, A., Proc. 12th International Conference on Automated Deduction (CADE’94). Proc. 12th International Conference on Automated Deduction (CADE’94), Lecture Notes in Artificial Intelligence, Vol. 814 (1994), Springer: Springer Berlin), 723-737 · Zbl 1433.03026
[55] Massacci, F., Simplification: A general constraint propagation technique for propositional and modal tableaux, (de Swart, H., Proc. 2nd International Conference on Analytic Tableaux and Related Methods (TABLEAUX’98). Proc. 2nd International Conference on Analytic Tableaux and Related Methods (TABLEAUX’98), Lecture Notes in Artificial Intelligence, Vol. 1397 (1998), Springer: Springer Berlin), 217-231 · Zbl 0903.03012
[56] Massacci, F., Tableaux methods for formal verification in multi-agent distributed systems, J. Logic Comput., Vol. 8, 3, 373-400 (1998) · Zbl 0904.68133
[57] Massacci, F., Single step tableaux for modal logics: Methodology, computations, algorithms, J. Automat. Reason., Vol. 24, 3, 319-364 (2000) · Zbl 0951.03008
[58] Massacci, F.; Donini, F. M., Design and results of TANCS-00, (Dyckhoff, R., Proc. 4th International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2000). Proc. 4th International Conference on Analytic Tableaux and Related Methods (TABLEAUX 2000), Lecture Notes in Artificial Intelligence, Vol. 1847 (2000), Springer: Springer Berlin) · Zbl 0963.68518
[59] Mehlhorn, K.; Nueher, S.; Seel, M.; Uhrig, C., The LEDA User Manual, http://www.mpi-sb.mpg.de/LEDA/ (1998), Max-Planck-Institut für Informatik and Algorithmic Solutions Software GmbH
[60] Nebel, B., Computational complexity of terminological reasoning in BACK, Artificial Intelligence, Vol. 34, 3, 371-383 (1988) · Zbl 0646.68110
[61] Nebel, B.; Bürckert, H.-J., Reasoning about temporal relations: A maximal tractable subclass of Allen’s interval algebra, J. ACM, Vol. 42, 1, 43-66 (1995) · Zbl 0886.68077
[62] Ohlbach, H. J., Translation methods for non-classical logics—An overview, J. Interest Group in Pure and Applied Logic, Vol. 1, 1, 69-89 (1993) · Zbl 0795.03019
[63] Oppacher, F.; Suen, E., HARP: A tableau-based theorem prover, J. Automat. Reason., Vol. 4, 69-100 (1988)
[64] Patel-Schneider, P., DLP system description, (Franconi, E.; etal., Proc. 1998 Internat. Workshop on Description Logics (1998), Technical Report ITC-IRST 9805-03), Available as CEUR Publication at http://SunSite.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/Vol-11/ · Zbl 0963.68525
[65] Pratt, V. R., A practical decision method for propositional dynamic logic, (Proc. 10th ACM Symposium on Theory of Computing (STOC’78), San Diego, CA (1978)), 326-337 · Zbl 1283.03066
[66] Pratt, V. R., Models of program logics, (Proc. 20th Annual Symposium on the Foundations of Computer Science (FOCS’79) (1979), IEEE Computer Society Press), 115-122
[67] Renz, J.; Nebel, B., On the complexity of qualitative spatial reasoning: A maximal tractable fragment of the region connection calculus, Artificial Intelligence, Vol. 108, 1-2, 69-123 (1999) · Zbl 0914.68160
[68] Schild, K., A correspondence theory for terminological logics: Preliminary report, (Proc. IJCAI-91, Sydney, Australia (1991), Morgan Kaufmann: Morgan Kaufmann Los Altos, CA), 466-471 · Zbl 0742.68059
[69] Schmidt, R., Decidability by resolution for propositional modal logics, J. Automat. Reason., Vol. 22, 4, 379-396 (1999) · Zbl 0924.68178
[70] Schmidt-Schauß, M.; Smolka, G., Attributive concept descriptions with complements, Artificial Intelligence, Vol. 48, 1-26 (1991) · Zbl 0712.68095
[71] Shanin, N.; Davydov, G. Yu.; Mints, G. E.; Orenkov, V. P.; Slisenko, A. O., An algorithm for machine search of a natural logical deduction in a propositional calculus, (Siekmann, J.; Wrightson, G., Automation of Reasoning (Classical Papers on Computational Logic), Vol. 1 (1957-1966) (1983), Springer: Springer Berlin)
[72] Smullyan, R. M., First Order Logic (1968), Springer: Springer Berlin, Republished by Dover, New York, 1995 · Zbl 0172.28901
[73] Smullyan, R. M., Uniform Gentzen systems, J. Symbolic Logic, Vol. 33, 4, 549-559 (1968) · Zbl 0197.27305
[74] Sundar, R.; Tarjan, R., Unique binary-search-tree representations and equality testing of sets and sequences, SIAM J. Comput., Vol. 23, 1, 24-44 (1994) · Zbl 0802.68035
[75] Tobies, S., A PSPACE algorithm for graded modal logic, (Ganzinger, H., Proc. 16th International Conference on Automated Deduction (CADE’99). Proc. 16th International Conference on Automated Deduction (CADE’99), Lecture Notes in Artificial Intelligence, Vol. 1632 (1999), Springer: Springer Berlin), 52-66 · Zbl 0937.03012
[76] Urquhart, A., The complexity of propositional proofs, Bull. Symbolic Logic, Vol. 1, 4, 425-467 (1995) · Zbl 0845.03025
[77] Vardi, M.; Wolper, P., Automata-theoretic techniques for modal logics of programs, J. Comput. System Sci., Vol. 32, 183-221 (1986) · Zbl 0622.03017
[78] Vardi, M.; Wolper, P., Reasoning about infinite computations, Inform. and Comput., Vol. 115, 1, 1-37 (1994) · Zbl 0827.03009
[79] Wright, J. R.; Weixelbaum, E. S.; Vesonder, G. T.; Brown, K. E.; Palmer, S. R.; Berman, J. I.; Moore, H. H., A knowledge-based configurator that supports sales, engineering, and manufacturing at AT&T network systems, AI Magazine, Vol. 14, 3, 69-80 (1993)
[80] Yellin, D., An algorithm for dynamic subset and intersection testing, Theoret. Comput. Sci., Vol. 129, 2, 397-406 (1994)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.