{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:10:04Z","timestamp":1749125404138,"version":"3.41.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2002,2,1]],"date-time":"2002-02-01T00:00:00Z","timestamp":1012521600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,2,1]],"date-time":"2002-02-01T00:00:00Z","timestamp":1012521600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2002,2]]},"DOI":"10.1023\/a:1015063215934","type":"journal-article","created":{"date-parts":[[2002,12,28]],"date-time":"2002-12-28T22:07:59Z","timestamp":1041113279000},"page":"173-204","source":"Crossref","is-referenced-by-count":3,"title":["Evaluating Optimized Decision Procedures for Propositional Modal K\n(m) Satisfiability"],"prefix":"10.1007","volume":"28","author":[{"given":"Ian","family":"Horrocks","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter F.","family":"Patel-Schneider","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"Baader, F.: Augmenting concept languages by transitive closure of roles: An alternative to terminological cycles, in Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI-91), 1991, pp. 446\u2013451.","key":"395294_CR1"},{"unstructured":"Baader, F. and Hanschke, P.: A scheme for integrating concrete domains into concept languages, in Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI-91), 1991, pp. 452\u2013457.","key":"395294_CR2"},{"doi-asserted-by":"crossref","unstructured":"Baader, F. and Hollunder, B.: A terminological knowledge representation system with complete inference algorithms, in Processing Declarative Knowledge: International Workshop PDK'91, Berlin, 1991, pp. 67\u201386.","key":"395294_CR3","DOI":"10.1007\/BFb0013522"},{"doi-asserted-by":"crossref","unstructured":"Baader, F. and Sattler, U.: Number restrictions on complex roles in description logics, in Principles of Knowledge Representation and Reasoning: Proceedings of the Fifth International Conference (KR'96), 1996, pp. 328\u2013339.","key":"395294_CR4","DOI":"10.25368\/2022.70"},{"unstructured":"Baker, A. B.: Intelligent backtracking on constraint satisfaction problems: Experimental and theoretical results, Ph.D. Thesis, University of Oregon, 1995.","key":"395294_CR5"},{"doi-asserted-by":"crossref","unstructured":"Balsiger, P. and Heuerding, A.: Comparison of theorem provers for modal logics \u2014 introduction and Summary, in H. de Swart (ed.), Automated Reasoning with Analytic Tableaux and Related Methods: International Conference Tableaux'98, 1998, pp. 25\u201326.","key":"395294_CR6","DOI":"10.1007\/3-540-69778-0_4"},{"key":"395294_CR7","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1613\/jair.21","volume":"1","author":"M. Buchheit","year":"1993","unstructured":"Buchheit, M., Donini, F.M. and Schaerf, A.: Decidable reasoning in terminological knowledge representation systems, J. Artificial Intelligence Res.\n1 (1993), 109\u2013138.","journal-title":"J. Artificial Intelligence Res."},{"key":"395294_CR8","volume-title":"Report on a SAT competition, Technical Report 110","author":"M. Buro","year":"1992","unstructured":"Buro, M. and Buning, H.: Report on a SAT competition, Technical Report 110, University of Paderborn, Germany, 1992."},{"key":"395294_CR9","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G. and Loveland, D.: A machine program for theorem proving, Comm. ACM\n5 (1962), 394\u2013397.","journal-title":"Comm. ACM"},{"unstructured":"Donini, F., Giacomo, G. D. and Massacci, F.: EXPTIME tableaux for ALC, in L. Padgham, E. Franconi, M. Gehrke, D. L. McGuinness, and P. F. Patel-Schneider (eds.), Collected Papers from the International Description Logics Workshop (DL'96), 1996, pp. 107\u2013110.","key":"395294_CR10"},{"key":"395294_CR11","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1016\/0166-218X(83)90017-3","volume":"5","author":"J. Franco","year":"1983","unstructured":"Franco, J. and Paull, M.: Probabilistic analysis of the Davis\u2014Putnam procedure for solving the satisfiability problem, Discrete Appl. Math. 5 (1983), 77\u201387.","journal-title":"Discrete Appl. Math"},{"unstructured":"Franconi, E., Giacomo, G. D., MacGregor, R. M., Nutt, W., Welty, C. A. and Sebastiani, F. (eds.), Collected Papers from the International Description Logics Workshop (DL'98), 1998.","key":"395294_CR12"},{"unstructured":"Freeman, J. W.: Improvements to propositional satisfiability search algorithms, Ph.D. Thesis, Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA, USA.","key":"395294_CR13"},{"key":"395294_CR14","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0004-3702(95)00051-8","volume":"81","author":"J. W. Freeman","year":"1996","unstructured":"Freeman, J. W.: Hard random 3-SAT problems and the Davis\u2014Putnam procedure, Artificial Intelligence\n81 (1996), 183\u2013198.","journal-title":"Artificial Intelligence"},{"unstructured":"Gent, I. P. and Walsh, T.: Beyond NP: The QSAT phase transition, in Proceedings of AAAI'99, Orlando, Florida, 1999.","key":"395294_CR15"},{"doi-asserted-by":"crossref","unstructured":"Giacomo, G. D. and Massacci, F.: Tableaux and algorithms for propositional dynamic logic with converse, in [34], pp. 613\u2013628.","key":"395294_CR16","DOI":"10.1007\/3-540-61511-3_117"},{"key":"395294_CR17","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1613\/jair.1","volume":"1","author":"M. L. Ginsberg","year":"1993","unstructured":"Ginsberg, M. L.: Dynamic backtracking, J. Artificial Intelligence Res.\n1 (1993), 25\u201346.","journal-title":"J. Artificial Intelligence Res."},{"unstructured":"Giunchiglia, E., Giunchiglia, F., Sebastiani, R. and Tacchella, A.: More evaluation of decision procedures for modal logics, in A. G. Cohn, L. Schubert, and S. C. Shapiro (eds.), Principles of Knowledge Representation and Reasoning: Proceedings of the Sixth International Conference (KR'98), 1998, pp. 626\u2013635.","key":"395294_CR18"},{"doi-asserted-by":"crossref","unstructured":"Giunchiglia, F. and Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures \u2014 the case study of modal K, in [34], pp. 583\u2013597.","key":"395294_CR19","DOI":"10.1007\/3-540-61511-3_115"},{"unstructured":"Giunchiglia, F. and Sebastiani, R.: A SAT-based decision procedure for ALC, in Principles of Knowledge Representation and Reasoning: Proceedings of the Fifth International Conference (KR'96), 1996, pp. 304\u2013314.","key":"395294_CR20"},{"unstructured":"Haarslev, V., M\u00f6ller, R. and Turhan, A.-Y.: Implementing an ALCRP(D) ABox Reasoner \u2014 Progress Report, in [12], pp. 82\u201386.","key":"395294_CR21"},{"key":"395294_CR22","series-title":"Technical Report","volume-title":"A benchmark method for the propositional modal logics K, KT, and S4","author":"A. Heuerding","year":"1996","unstructured":"Heuerding, A. and Schwendimann, S.: A benchmark method for the propositional modal logics K, KT, and S4, Technical Report IAM-96-015, University of Bern, Switzerland, 1996."},{"unstructured":"Hollunder, B. and Nutt, W.: Subsumption algorithms for concept languages, Research Report RR-90-04, Deutsches Forschungszentrum f\u00fcr K\u00fcnstliche Intelligenz GmbH (DFKI), 1990.","key":"395294_CR23"},{"unstructured":"Horrocks, I.: Optimising tableaux decision procedures for description logics, Ph.D. Thesis, University of Manchester, 1997.","key":"395294_CR24"},{"unstructured":"Horrocks, I.: Using an expressive description logic: FaCT or fiction?, in A. G. Cohn, L. Schubert, and S. C. Shapiro (eds.), Principles of Knowledge Representation and Reasoning: Proceedings of the Sixth International Conference (KR'98), 1998, pp. 636\u2013647.","key":"395294_CR25"},{"unstructured":"Horrocks, I. and Patel-Schneider, P. F.: Comparing subsumption optimizations, in [12], pp. 90\u201394.","key":"395294_CR26"},{"doi-asserted-by":"crossref","unstructured":"Horrocks, I. and Patel-Schneider, P. F.: FaCT and DLP, in H. de Swart (ed.), Automated Reasoning with Analytic Tableaux and Related Methods: International Conference Tableaux'98, 1998, pp. 27\u201330.","key":"395294_CR27","DOI":"10.1007\/3-540-69778-0_5"},{"doi-asserted-by":"crossref","unstructured":"Horrocks, I. and Patel-Schneider, P. F.: Optimising propositional modal satisfiability for description logic subsumption, in International Conference AISC'98, 1998.","key":"395294_CR28","DOI":"10.1007\/BFb0055916"},{"key":"395294_CR29","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1093\/logcom\/9.3.267","volume":"9","author":"I. Horrocks","year":"1999","unstructured":"Horrocks, I. and Patel-Schneider, P. F.: Optimizing description logic subsumption, J. Logic Comput.\n9 (1999), 267\u2013293.","journal-title":"J. Logic Comput."},{"key":"395294_CR30","doi-asserted-by":"crossref","first-page":"385","DOI":"10.1093\/logcom\/9.3.385","volume":"9","author":"I. Horrocks","year":"1999","unstructured":"Horrocks, I. and Sattler, U.: A description logic with transitive and inverse roles and role hierarchies, J. Logic Comput.\n9 (1999), 385\u2013410.","journal-title":"J. Logic Comput."},{"unstructured":"Hustadt, U. and Schmidt, R. A.: On evaluating decision procedures for modal logic, Technical Report MPI-I-97-2-003, Max-Planck-Institut f\u00fcr Informatik, Im Stadtwald, D 66123 Saarbr\u00fccken, Germany, 1997.","key":"395294_CR31"},{"key":"395294_CR32","first-page":"202","volume":"1","author":"U. Hustadt","year":"1997","unstructured":"Hustadt, U. and Schmidt, R. A.: On evaluating decision procedures for modal logic, in Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97), Vol. 1, 1997, pp. 202\u2013207.","journal-title":"Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97)"},{"key":"395294_CR33","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/BF01531077","volume":"1","author":"R. Jeroslow","year":"1990","unstructured":"Jeroslow, R. and Wang, J.: Solving propositional satisfiability problems, Ann. Math. Artif. Intell.\n1 (1990), 167\u2013187.","journal-title":"Ann. Math. Artif. Intell."},{"doi-asserted-by":"crossref","unstructured":"McRobbie, M. and Slaney, J. (eds.): Proceedings of the Thirteenth International Conference on Automated Deduction (CADE-13), Lecture Notes in Artificial Intelligence 1104, Springer-Verlag, 1996.","key":"395294_CR34","DOI":"10.1007\/3-540-61511-3"},{"key":"395294_CR35","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/BF00244513","volume":"4","author":"F. Oppacher","year":"1988","unstructured":"Oppacher, F. and Suen, E.: HARP: A tableau-based theorem prover, J. Automated Reasoning\n4 (1988), 69\u2013100.","journal-title":"J. Automated Reasoning"},{"unstructured":"Patel-Schneider, P. F.: DLP system description, in [12], pp. 87\u201389.","key":"395294_CR36"},{"doi-asserted-by":"crossref","unstructured":"Sattler, U.: A concept language extended with different kinds of transitive roles, in G. G\u00f6rz and S. H\u00f6lldobler (eds.), 20. Deutsche Jahrestagung f\u00fcr K\u00fcnstliche Intelligenz, 1996, pp. 333\u2013345.","key":"395294_CR37","DOI":"10.1007\/3-540-61708-6_74"},{"key":"395294_CR38","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/0004-3702(95)00045-3","volume":"81","author":"B. Selman","year":"1996","unstructured":"Selman, B., Mitchell, D. G. and Levesque, H. J.: Generating hard satisfiability problems, Artificial Intelligence\n81 (1996), 17\u201329.","journal-title":"Artificial Intelligence"},{"unstructured":"Vellino, A.: The complexity of automated reasoning, Ph.D. Thesis, University of Toronto, 1989.","key":"395294_CR39"},{"doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Gaede, B., and Rock, G.: SPASS & FLOTTER version 0.42, in [34], pp. 141\u2013145.","key":"395294_CR40","DOI":"10.1007\/3-540-61511-3_75"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1015063215934.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1015063215934\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1015063215934.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:34:22Z","timestamp":1749123262000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1015063215934"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,2]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,2]]}},"alternative-id":["395294"],"URL":"https:\/\/doi.org\/10.1023\/a:1015063215934","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2002,2]]}}}