{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:16:51Z","timestamp":1725488211260},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540644064"},{"type":"electronic","value":"9783540697787"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-69778-0_30","type":"book-chapter","created":{"date-parts":[[2007,8,4]],"date-time":"2007-08-04T05:02:30Z","timestamp":1186203750000},"page":"307-312","source":"Crossref","is-referenced-by-count":88,"title":["The FaCT System"],"prefix":"10.1007","author":[{"given":"Ian","family":"Horrocks","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,7,21]]},"reference":[{"issue":"1\u20132","key":"30_CR1","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1016\/S0004-3702(96)00010-0","volume":"88","author":"F. Baader","year":"1996","unstructured":"F. Baader, M. Buchheit, and B. Hollunder. Cardinality restrictions on concepts. Artificial Intelligence, 88(1\u20132):195\u2013213, 1996.","journal-title":"Artificial Intelligence"},{"key":"30_CR2","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, Principals of Knowledge Representation and Reasoning: Proceedings of the Third International Conference (KR\u201992), pages 270\u2013281. Morgan-Kaufmann, 1992. Also available as DFKI RR-93-03."},{"key":"30_CR3","unstructured":"F. Baader, H.-J. Heinsohn, B. Hollunder, J. Muller, B. Nebel, W. Nutt, and H.-J. Profitlich. Terminological knowledge representation: A proposal for a terminological logic. Technical Memo TM-90-04, Deutsches Forschungszentrum f\u00fcr K\u00fcnstliche Intelligenz GmbH (DFKI), 1991."},{"issue":"3","key":"30_CR4","doi-asserted-by":"publisher","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":"30_CR5","unstructured":"A. B. Baker. Intelligent Backtracking on Constraint Satisfaction Problems: Experimental and Theoretical Results. PhD thesis, University of Oregon, 1995."},{"key":"30_CR6","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":"30_CR7","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1613\/jair.21","volume":"1","author":"M. Buchheit","year":"1993","unstructured":"M. Buchheit, F. M. Donini, and A. Schaerf. Decidable reasoning in terminological knowledge representation systems. Journal of Artificial Intelligence Research, 1:109\u2013138, 1993.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"30_CR8","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":"30_CR9","volume-title":"Improvements to propositional satisfiability search algorithms","author":"J. W. Freeman","year":"1995","unstructured":"J. W. Freeman. Improvements to propositional satisfiability search algorithms. PhD thesis, Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA, USA, 1995."},{"key":"30_CR10","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":"30_CR11","doi-asserted-by":"crossref","unstructured":"F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures\u2014the case study of modal K. In Michael McRobbie and John Slaney, editors, Proceedings of the Thirteenth International Conference on Automated Deduction (CADE-13), number 1104 in Lecture Notes in Artificial Intelligence, pages 583\u2013597. Springer, 1996.","DOI":"10.1007\/3-540-61511-3_115"},{"key":"30_CR12","unstructured":"F. Giunchiglia and R. Sebastiani. A SAT-based decision procedure for ALC. In L. C. Aiello, J. Doyle, and S. Shapiro, editors, Principals of Knowledge Representation and Reasoning: Proceedings of the Fifth International Conference (KR\u201996), pages 304\u2013314. Morgan Kaufmann, November 1996."},{"key":"30_CR13","series-title":"Technical report","volume-title":"A benchmark method for the propositional modal logics k, kt, s4","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":"30_CR14","unstructured":"I. Horrocks. Optimising Tableaux Decision Procedures for Description Logics. PhD thesis, University of Manchester, 1997."},{"key":"30_CR15","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":"30_CR16","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":"30_CR17","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."},{"key":"30_CR18","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0004-3702(91)90078-X","volume":"48","author":"M. Schmidt-Schau\u00df","year":"1991","unstructured":"M. Schmidt-Schau\u00df and G. Smolka. Attributive concept descriptions with complements. Artificial Intelligence, 48:1\u201326, 1991.","journal-title":"Artificial Intelligence"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-69778-0_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T15:07:15Z","timestamp":1556723235000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-69778-0_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540644064","9783540697787"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-69778-0_30","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}