{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T09:32:34Z","timestamp":1742635954547},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"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-58156-1_7","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:24:32Z","timestamp":1330269872000},"page":"87-101","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Model elimination without contrapositives"],"prefix":"10.1007","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[]},{"given":"Ulrich","family":"Furbach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1145\/321592.321603","volume":"17","author":"R. Anderson","year":"1970","unstructured":"R. Anderson and W. Bledsoe. A linear format for resolution with merging and a new technique for establishing completeness. J. of the ACM, 17:525\u2013534, 1970.","journal-title":"J. of the ACM"},{"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.","key":"7_CR2","DOI":"10.1007\/3-540-55602-8_168"},{"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.","key":"7_CR3","DOI":"10.1007\/BFb0018990"},{"doi-asserted-by":"crossref","unstructured":"P. Baumgartner and U. Furbach. Consolution as a Framework for Comparing Calculi. Journal of Symbolic Computation, 16(5), 1993.","key":"7_CR4","DOI":"10.1006\/jsco.1993.1058"},{"doi-asserted-by":"crossref","unstructured":"P. Baumgartner and U. Furbach. PROTEIN: A PROver with a Theory Extension Interface. In 12th International Conference on Automated Deduction. Springer, 1994. (in this volume).","key":"7_CR5","DOI":"10.1007\/3-540-58156-1_57"},{"doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg, 2nd edition, 1987.","key":"7_CR6","DOI":"10.1007\/978-3-322-90102-6"},{"unstructured":"E. Eder. Consolution and its Relation with Resolution. In Proc. IJCAI '91, 1991.","key":"7_CR7"},{"doi-asserted-by":"crossref","unstructured":"E. Eder. Relative Complexities of First Order Languages. Vieweg, 1992.","key":"7_CR8","DOI":"10.1007\/978-3-322-84222-0"},{"doi-asserted-by":"crossref","unstructured":"M. Fitting. First-Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, 1990.","key":"7_CR9","DOI":"10.1007\/978-1-4684-0357-2"},{"issue":"4","key":"7_CR10","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/S0743-1066(85)80003-0","volume":"2","author":"D. M. Gabbay","year":"1985","unstructured":"D. M. Gabbay. N-Prolog: An extension of Prolog with hypothetical implication II. logical foundations, and negation as failure. The Journal of Logic Programming, 2(4):251\u2013284, December 1985.","journal-title":"The Journal of Logic Programming"},{"unstructured":"J. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Proving. Wiley, 1987.","key":"7_CR11"},{"doi-asserted-by":"crossref","unstructured":"R. Letz, K. Mayr, and C. Goller. Controlled Integrations of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning (to appear 1994), 1993.","key":"7_CR12","DOI":"10.1007\/BF00881947"},{"doi-asserted-by":"crossref","unstructured":"D. Loveland. Mechanical Theorem Proving by Model Elimination. JACM, 15(2), 1968.","key":"7_CR13","DOI":"10.1145\/321450.321456"},{"key":"7_CR14","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"},{"unstructured":"D.W. Loveland and D.W. Reed. A near-horn prolog for compilation. Technical Report CS-1989-14, Duke University, 1989.","key":"7_CR15"},{"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.","key":"7_CR16","DOI":"10.1007\/BF00244282"},{"key":"7_CR17","volume-title":"SLWV \u2014 A Theorem Prover for Logic Programming","author":"L. M. Pereira","year":"1991","unstructured":"L. M. Pereira, L. Caires, and J. Alferes. SLWV \u2014 A Theorem Prover for Logic Programming. AI Centre, Uninova, Portugal, July 1991."},{"key":"7_CR18","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"D. Plaisted","year":"1988","unstructured":"D. Plaisted. Non-Horn Clause Logic Programming Without Contrapositives. Journal of Automated Reasoning, 4:287\u2013325, 1988.","journal-title":"Journal of Automated Reasoning"},{"issue":"6","key":"7_CR19","first-page":"389","volume":"4","author":"D. Plaisted","year":"1990","unstructured":"D. Plaisted. A Sequent-Style Model Elimination Strategy and a Positive Refinement. Journal of Automated Reasoning, 4(6):389\u2013402, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR20","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0743-1066(92)90038-5","volume":"12","author":"D. W. Reed","year":"1992","unstructured":"D. W. Reed and D. W. Loveland. A Comparison of Three Prolog Extensions. Journal of Logic Programming, 12:25\u201350, 1992.","journal-title":"Journal of Logic Programming"},{"doi-asserted-by":"crossref","unstructured":"G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP problem library. In Proc. CADE-12. Springer, 1994.","key":"7_CR21","DOI":"10.1007\/3-540-58156-1_18"},{"key":"7_CR22","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"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:21:35Z","timestamp":1558268495000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]},"assertion":[{"value":"30 May 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}