{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T12:59:38Z","timestamp":1790686778308,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540578024","type":"print"},{"value":"9783540483359","type":"electronic"}],"license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57802-1_8","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:23:20Z","timestamp":1330262600000},"page":"139-156","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Theory reasoning in first order calculi"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"Furbach","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,5,28]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Owen L. Astrachan and Mark E. Stickel. Caching and Lemmaizing in Model Elimination Theorem Provers. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction (CADE-11), pages 224\u2013238. Springer-Verlag, June 1992. LNAI 607.","DOI":"10.1007\/3-540-55602-8_168"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"P. Baumgartner. A Model Elimination Calculus with Built-in Theories. In H.-J. Ohlbach, editor, Proceedings of the 16-th German AI-Conference (GWAI-92), pages 30\u201342. Springer, 1992. LNAI 671.","DOI":"10.1007\/BFb0018990"},{"key":"8_CR3","unstructured":"P. Baumgartner. Linear Completion: Combining the Linear and the Unit-Resulting Restrictions. Research Report 9\/93, University of Koblenz, 1993. (submitted)."},{"key":"8_CR4","unstructured":"P. Baumgartner. Refinements of Theory Model Elimination and a Variant without Contrapositives. Research Report 8\/93, University of Koblenz, 1993."},{"key":"8_CR5","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 termininological knowledge representation systems. Journal of Artificial Intelligence Research, 1:109\u2013138, 1993.","journal-title":"Journal of Artificial Intelligence Research"},{"key":"8_CR6","unstructured":"P. Baumgartner and U. Furbach. Consolution as a Framework for Comparing Calculi. Forschungsbericht 11\/92, University of Koblenz, 1992. (to appear in Journal of Symbolic Computation)."},{"key":"8_CR7","unstructured":"P. Baumgartner and U. Furbach. Model Elimination without Contrapositives and its Application to PTTP. Fachbericht Informatik 12\/93, Universit\u00e4t Koblenz, 1993. (submitted)."},{"issue":"10","key":"8_CR8","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1109\/MC.1983.1654200","volume":"16","author":"R. Brachmann","year":"1983","unstructured":"R. Brachmann, R. Fikes, and H. Levesque. KRYPTON: a functional approach to knowledge representation. IEEE Computer, 16(10):67\u201373, October 1983.","journal-title":"IEEE Computer"},{"key":"8_CR9","unstructured":"Peter Baumgartner, Ulrich Furbach, and Uwe Petermann. A unified approach to theory reasoning. To appear."},{"key":"8_CR10","unstructured":"R. Brachman, V. Gilbert, and H. Levesque. An Essential Hybrid Reasoning System: Knowledge and Symbol Level Accounts of Krypton. In Proc. IJCAI, 1985."},{"key":"8_CR11","unstructured":"C. Chang and R. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973."},{"key":"8_CR12","unstructured":"E. Eder. Consolution and its Relation with Resolution. In Proc. IJCAI '91, 1991."},{"key":"8_CR13","unstructured":"T. Fr\u00fchwirt and P. Hanschke. Terminological reasoning with constraint handling rules. Manuscript ECRC Munich, 1993."},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"M. Fitting. First Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"B. Hollunder. Hybrid Inferences in KL-ONE-based Knowledge Representation Systems. Research Report RR-90-6, DFKI, May 1990.","DOI":"10.1007\/978-3-642-76071-6_5"},{"key":"8_CR16","unstructured":"Otthein Herzog and Claus-Rainer Rollinger. Text Understanding in LILOG \u2014 Integrating Computational Linguistics and Artificial Intelligence, Final Report on the IBM Germany LILOG-Project. Springer-Verlag, 1991. LNAI 546."},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"W. Kie\u00dfling and U. G\u00fcnzer. Database reasoning \u2014 a deductive framework for solving large and complex problems by means of subsumption. This volume, 1993.","DOI":"10.1007\/3-540-57802-1_7"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Mohammed Nadjib Khenkhar. Eine objektorientierte Darstellung von Depiktionen auf der Grundlage von Zellmatrizen. In C. Freksa and C. Habel, editors, Repr\u00e4sentation und Verarbeitung r\u00e4umlichen Wissens, pages 99\u2013112. Springer-Verlag, 1990. Informatik-Fachberichte 245.","DOI":"10.1007\/978-3-642-84235-1_8"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"J. Lloyd. Foundations of Logic Programming. Symbolic Computation. Springer, second, extended edition, 1987.","DOI":"10.1007\/978-3-642-83189-8"},{"key":"8_CR20","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00249353","volume":"7","author":"D. Loveland","year":"1991","unstructured":"D. Loveland. Near-Horn Prolog and Beyond. Journal of Automated Reasoning, 7:1\u201326, 1991.","journal-title":"Journal of Automated Reasoning"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A High-Performace Theorem Prover. Journal of Automated Reasoning, 8(2), 1992.","DOI":"10.1007\/BF00244282"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"P. Meseguer. Constraint Satisfaction Problems: An Overview. AICOM, 2(1), March 1989.","DOI":"10.3233\/AIC-1989-2101"},{"key":"8_CR23","unstructured":"J\u00f6rg-Peter Mohren and J\u00fcrgen M\u00fcller. A geometrical approach to depicitonal representation of spatial relations. In Proc. of ECAI, 1992."},{"key":"8_CR24","unstructured":"U. Petermann. How to build in an open theory into connection calculi. submitted to J. on Computers and Artificial Intelligence, 1991."},{"key":"8_CR25","unstructured":"U. Petermann. Completeness of the pool calculus with an open built in theory. In Georg Gottlob, Alexander Leitsch, and Daniele Mundici, editors, 3rd Kurt G\u00f6del Colloquium '93, number 713 in Lecture Notes in Computer Science, pages 264\u2013277. Springer-Verlag, 1993."},{"issue":"1","key":"8_CR26","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"J\u00f6rg H. H. Siekmann","year":"1989","unstructured":"J\u00f6rg H. Siekmann. Unification Theory. Journal of Symbolic Computation, 7(1):207\u2013274, January 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"8_CR27","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M. E. Stickel","year":"1985","unstructured":"M.E. Stickel. Automated Deduction by Theory Resolution. Journal of Automated Reasoning, 1:333\u2013355, 1985.","journal-title":"Journal of Automated Reasoning"},{"key":"8_CR28","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/BF00246025","volume":"2","author":"M. Stickel","year":"1986","unstructured":"M. Stickel. Schubert's Steamroller Problem: Formulations and Solutions. Journal of Automated Reasoning, 2:89\u2013101, 1986.","journal-title":"Journal of Automated Reasoning"},{"key":"8_CR29","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. Stickel","year":"1988","unstructured":"M. Stickel. A Prolog Technology Theorem Prover: Implementation by an Extended Prolog Compiler. Journal of Automated Reasoning, 4:353\u2013380, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"8_CR30","volume-title":"Logic Programming","author":"P. Hentenryck Van","year":"1989","unstructured":"Pascal Van Hentenryck. Constraint Satisfaction in Logic Programming. Logic Programming. The MIT Press, Cambridge, Massachusetts, USA\/London, England, UK, 1989."}],"container-title":["Lecture Notes in Computer Science","Management and Processing of Complex Data Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57802-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T05:44:15Z","timestamp":1640929455000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57802-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578024","9783540483359"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-57802-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]},"assertion":[{"value":"28 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}