{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:42Z","timestamp":1749124062371},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649601"},{"type":"electronic","value":"9783540498162"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055916","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T17:17:34Z","timestamp":1154020654000},"page":"234-246","source":"Crossref","is-referenced-by-count":11,"title":["Optimising propositional modal satisfiability for description logic subsumption"],"prefix":"10.1007","author":[{"given":"Ian","family":"Horrocks","sequence":"first","affiliation":[]},{"given":"Peter F.","family":"Patel-Schneider","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"19_CR1","first-page":"270","volume-title":"An empirical analysis of optimization techniques for terminological representation systems or: Making KRIS get a move on","author":"F. Baader","year":"1992","unstructured":"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. In B. Nebel, C. Rich, and W. Swartout, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Third International Conference (KR\u201992), pages 270\u2013281. Morgan-Kaufmann Publishers, San Francisco, CA, 1992. Also available as DFKI RR-93-03."},{"issue":"3","key":"19_CR2","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1145\/122296.122298","volume":"2","author":"F. Baader","year":"1991","unstructured":"F. Baader and B. Hollunder. Kris: Knowledge representation and inference system. SIGART Bulletin, 2(3):8\u201314, 1991.","journal-title":"SIGART Bulletin"},{"key":"19_CR3","unstructured":"A. B. Baker. Intelligent Backtracking on Constraint Satisfaction Problems: Experimental and Theoretical Results. PhD thesis, University of Oregon, 1995."},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"P. Balsiger and A. Heuerding. Comparison of theorem provers for modal logics \u2014 introduction and summary. In H. de Swart, editor, Automated Reasoning with Analytic Tableaux and Related Methods: International Conference Tableaux\u201998, number 1397 in Lecture Notes in Artificial Intelligence, pages 25\u201326. Springer-Verlag, May 1998.","DOI":"10.1007\/3-540-69778-0_4"},{"key":"19_CR5","unstructured":"P. Bresciani, E. Franconi, and S. Tessaris. Implementing and testing expressive description logics: a preliminary report. In Gerard Ellis, Robert A. Levinson, Andrew Fall, and Veronica Dahl, editors, Knowledge Retrieval, Use and Storage for Efficiency: Proceedings of the First International KRUSE Symposium, pages 28\u201339, 1995."},{"key":"19_CR6","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"M. Davis, G. Logemann, and D. Loveland. A machine program for theorem proving. Communications of the ACM, 5:394\u2013397, 1962.","journal-title":"Communications of the ACM"},{"key":"19_CR7","first-page":"107","volume-title":"number WS-96-05 in AAAI Technical Report","author":"F. Donini","year":"1996","unstructured":"F. Donini, G. De Giacomo, and F. Massacci. EXPTIME tableaux for ACC. In L. Padgham, E. Franconi, M. Gehrke, D. L. McGuinness, and P. F. Patel-Schneider, editors, Collected Papers from the International Description Logics Workshop (DL\u201996), number WS-96-05 in AAAI Technical Report, pages 107\u2013110. AAAI Press, Menlo Park, California, 1996."},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0004-3702(95)00051-8","volume":"81","author":"J. W. Freeman","year":"1996","unstructured":"J. W. Freeman. Hard random 3-SAT problems and the Davis-Putnam procedure. Artificial Intelligence, 81:183\u2013198, 1996.","journal-title":"Artificial Intelligence"},{"key":"19_CR9","first-page":"304","volume-title":"A SAT-based decision procedure for ALC","author":"F. Giunchiglia","year":"1996","unstructured":"F. Giunchiglia and R. Sebastiani. A SAT-based decision procedure for ALC. In L. C. Aiello, J. Doyle, and S. Shapiro, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Fifth International Conference (KR \u201996), pages 304\u2013314. Morgan Kaufmann Publishers, San Francisco, CA, November 1996."},{"key":"19_CR10","volume-title":"Technical report IAM-96-015","author":"A. Heuerding","year":"1996","unstructured":"A. Heuerding and S. Schwendimann. A benchmark method for the propositional modal logics k, kt, s4. Technical report IAM-96-015, University of Bern, Switzerland, October 1996."},{"key":"19_CR11","unstructured":"I. Horrocks. Optimising Tableaux Decision Procedures for Description Logics. PhD thesis, University of Manchester, 1997."},{"key":"19_CR12","volume-title":"Technical Report MPI-I-97-2-003","author":"U. Hustadt","year":"1997","unstructured":"U. Hustadt and R. A. Schmidt. 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, February 1997."},{"key":"19_CR13","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF00244513","volume":"4","author":"F. Oppacher","year":"1988","unstructured":"F. Oppacher and E. Suen. HARP: A tableau-based theorem prover. Journal of Automated Reasoning, 4:69\u2013100, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR14","volume-title":"System description: DLP","author":"P. F. Patel-Schneider","year":"1997","unstructured":"P. F. Patel-Schneider. System description: DLP. Bell Labs Research, Murray Hill, NJ, December 1997."},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"U. Sattler. A concept language extended with different kinds of transitive roles. In G. G\u00f6rz and S. H\u00f6lldobler, editors, 20. Deutsche Jahrestagung f\u00fcr K\u00fcnstliche Intelligenz, number 1137 in Lecture Notes in Artificial Intelligence, pages 333\u2013345. Springer Verlag, 1996.","DOI":"10.1007\/3-540-61708-6_74"},{"key":"19_CR16","unstructured":"K. Schild. A correspondence theory for terminological logics: Preliminary report. In Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI-91), pages 466\u2013471, 1991."}],"container-title":["Lecture Notes in Computer Science","Artificial Intelligence and Symbolic Computation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055916","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T05:09:12Z","timestamp":1555736952000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055916"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649601","9783540498162"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/bfb0055916","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}