{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T12:10:01Z","timestamp":1749125401574,"version":"3.41.0"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1998,6,1]],"date-time":"1998-06-01T00:00:00Z","timestamp":896659200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1998,6,1]],"date-time":"1998-06-01T00:00:00Z","timestamp":896659200000},"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":[[1998,6]]},"DOI":"10.1023\/a:1005866922570","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T23:56:21Z","timestamp":1040514981000},"page":"337-364","source":"Crossref","is-referenced-by-count":10,"title":["Automated Deduction Techniques for Classification in Description Logic Systems"],"prefix":"10.1007","volume":"20","author":[{"given":"M.","family":"Paramasivam","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David A.","family":"Plaisted","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"142177_CR1","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 Research\n1 (1993), 109\u2013138.","journal-title":"J. Artificial Intelligence Research"},{"key":"142177_CR2","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1145\/122296.122298","volume":"2","author":"F. Baader","year":"1991","unstructured":"Baader, F. and Hollunder, B.: KRIS: Knowledge representation and inference system, SIGART Bulletin\n2 (1991), 22\u201327.","journal-title":"SIGART Bulletin"},{"key":"142177_CR3","unstructured":"Baader, F., Hollunder, B., Nebel, B., Profitlich, H-J. and Franconi, E.: An empirical analysis of optimization techniques for terminological representation systems, In Principles of Knowledge Representation and Reasoning \u2013 Proceedings of the 3rd International Conference, 1992."},{"key":"142177_CR4","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1613\/jair.56","volume":"1","author":"A. Borgida","year":"1994","unstructured":"Borgida, A. and Patel-Schneider, P. F.: A semantics and complete algorithm for subsumption in the classic description logic, J. Artificial Intelligence Research\n1 (1994), 277\u2013308.","journal-title":"J. Artificial Intelligence Research"},{"key":"142177_CR5","first-page":"171","volume":"9","author":"R. J. Brachman","year":"1985","unstructured":"Brachman, R. J. and Schmolze, J. G.: An overview of the KL-ONE knowledge representation system, Cognitive Science\n9 (1985), 171\u2013216.","journal-title":"Cognitive Science"},{"key":"142177_CR6","unstructured":"Chu, H.: CLIN-S User's Manual, 1994."},{"key":"142177_CR7","volume-title":"Generating unit consequences of a ground clause set","author":"H. Chu","year":"1992","unstructured":"Chu, H. and Plaisted, D.: Generating unit consequences of a ground clause set, Technical report, University of North Carolina, Chapel Hill, N.C., 1992."},{"key":"142177_CR8","doi-asserted-by":"crossref","first-page":"221","DOI":"10.3233\/FI-1994-2134","volume":"21","author":"H. Chu","year":"1994","unstructured":"Chu, H. and Plaisted, D. A.: Model finding in semantically guided instance-based theorem proving, Fundamenta Informaticae\n21 (1994), 221\u2013235.","journal-title":"Fundamenta Informaticae"},{"key":"142177_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0357-2","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M. Fitting","year":"1990","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving, Springer-Verlag, New York, 1990."},{"key":"142177_CR10","doi-asserted-by":"crossref","unstructured":"Fermuller, C., Leitsch, A., Tammet, T. and Zamov, N.: Resolution Methods and the Decision Problem, Springer-Verlag, 1993. Lecture Notes in Artificial Intelligence, 679.","DOI":"10.1007\/3-540-56732-1"},{"key":"142177_CR11","unstructured":"Gelder, V.: Personal communication."},{"key":"142177_CR12","series-title":"Technical report, DFKI Research Report","volume-title":"An emperical analysis of terminological representation systems","author":"J. Heinsohn","year":"1992","unstructured":"Heinsohn, J., Kudenko, D., Nebel, B. and Profitlich, H.: An emperical analysis of terminological representation systems, Technical report, DFKI Research Report, German Research Center for Artificial Intelligence (DFKI), Kaiserlautern, 1992."},{"key":"142177_CR13","series-title":"Technical report, DFKI Research Report","volume-title":"Subsumption algorithms for concept languages","author":"B. Hollunder","year":"1990","unstructured":"Hollunder, B. and Nutt, W.: Subsumption algorithms for concept languages, Technical report, DFKI Research Report RR-90-04, German Research Center for Artificial Intelligence (DFKI), Kaiserlautern, 1990."},{"key":"142177_CR14","volume-title":"CLIN: An Automated Reasoning System Using Clause Linking","author":"S-J. Lee","year":"1990","unstructured":"Lee, S-J.: CLIN: An Automated Reasoning System Using Clause Linking, PhD thesis, University of North Carolina at Chapel Hill, 1990."},{"key":"142177_CR15","first-page":"25","volume":"9","author":"S-J. Lee","year":"1992","unstructured":"Lee, S-J. and Plaisted, D. A.: Eliminating duplication with the hyper-linking strategy, J. Automated Reasoning\n9 (1992), 25\u201342.","journal-title":"J. Automated Reasoning"},{"key":"142177_CR16","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1023\/A:1005847700447","volume":"18","author":"M. Paramasivam","year":"1997","unstructured":"Paramasivam, M. and Plaisted, D. A.: RRTP: A Replacement Rule Theorem Prover, J. Automated Reasoning\n18 (1997), 221\u2013226.","journal-title":"J. Automated Reasoning"},{"key":"142177_CR17","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1145\/122296.122309","volume":"2","author":"R. MacGregor","year":"1991","unstructured":"MacGregor, R.: Inside the LOOM description classifier, SIGART Bulletin\n2 (1991), 88\u201382.","journal-title":"SIGART Bulletin"},{"key":"142177_CR18","volume-title":"OTTER 2.0 Users Guide","author":"W. W. McCune","year":"1990","unstructured":"McCune, W. W.: OTTER 2.0 Users Guide, Argonne National Laboratory, Argonne, Illinois, 1990."},{"key":"142177_CR19","volume-title":"Reasoning and Revision in Hybrid Representation Systems","author":"B. Nebel","year":"1990","unstructured":"Nebel, B.: Reasoning and Revision in Hybrid Representation Systems, Springer-Verlag, Berlin, Germany, 1990."},{"key":"142177_CR20","doi-asserted-by":"crossref","first-page":"114","DOI":"10.1145\/122296.122314","volume":"2","author":"C. Petalson","year":"1991","unstructured":"Petalson, C.: The BACK system \u2013 an overview, SIGART Bulletin\n2 (1991), 114\u2013119.","journal-title":"SIGART Bulletin"},{"key":"142177_CR21","unstructured":"Plaisted, D. A.: Theorem Proving and Semantic Trees, PhD thesis, Stanford University, 1976."},{"key":"142177_CR22","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"D. A. Plaisted","year":"1988","unstructured":"Plaisted, D. A.: Non-Horn clause logic programming without contrapositives, J. Automated Reasoning\n4 (1988), 287\u2013325.","journal-title":"J. Automated Reasoning"},{"key":"142177_CR23","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1145\/122296.122313","volume":"2","author":"P. F. Patel-Schneider","year":"1991","unstructured":"Patel-Schneider, P. F., McGuiness, D. L., Brachman, R. J., Alperin Resnick, L. and Borgida, A.: The CLASSIC knowledge representation system: Guiding principles and implementational rational, SIGART Bulletin\n2 (1991), 108\u2013113.","journal-title":"SIGART Bulletin"},{"key":"142177_CR24","unstructured":"Zhang, H.: Personal communication."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005866922570.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005866922570\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005866922570.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:31:10Z","timestamp":1749123070000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005866922570"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998,6]]},"references-count":24,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1998,6]]}},"alternative-id":["142177"],"URL":"https:\/\/doi.org\/10.1023\/a:1005866922570","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1998,6]]}}}