{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T03:11:35Z","timestamp":1761621095472},"publisher-location":"Berlin, Heidelberg","reference-count":17,"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_57","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:24:21Z","timestamp":1330251861000},"page":"769-773","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":24,"title":["Protein: A PROver with a Theory Extension INterface"],"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":"57_CR1","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":"57_CR2","unstructured":"P. Baumgartner. Linear Completion: Combining the Linear and the Unit-Resulting Restrictions. Research Report 9\/93, University of Koblenz, 1993."},{"key":"57_CR3","doi-asserted-by":"crossref","unstructured":"P. Baumgartner. Refinements of Theory Model Elimination and a Variant without Contrapositives. In Proc. ECAI'94, 1994. (to appear).","DOI":"10.1007\/3-540-58156-1_7"},{"key":"57_CR4","doi-asserted-by":"crossref","unstructured":"P. Baumgartner and U. Furbach. Model Elimination without Contrapositives and its Application to PTTP. Fachbericht Informatik 12\/93, Universit\u00e4t Koblenz, 1993. (short version in Proc. CADE-12).","DOI":"10.1007\/3-540-58156-1_7"},{"key":"57_CR5","doi-asserted-by":"crossref","unstructured":"P. Baumgartner and U. Furbach. Model Elimination without Contrapositives. In Proc. 12th International Conference on Automated Deduction. Springer, 1994. (in this volume).","DOI":"10.1007\/3-540-58156-1_7"},{"key":"57_CR6","unstructured":"P. Baumgartner, U. Furbach, and U. Petermann. A Unified Approach to Theory Reasoning. Forschungsbericht 15\/92, University of Koblenz, 1992. (submitted to Journal of Automated Reasoning)."},{"key":"57_CR7","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/BF00244493","volume":"6","author":"W. W. Bledsoe","year":"1990","unstructured":"W. W. Bledsoe. Challenge Problems in Elementary Calculus. Journal of Automated Reasoning, 6:341\u2013359, 1990.","journal-title":"Journal of Automated Reasoning"},{"key":"57_CR8","unstructured":"Manfred Kerber, Erica Melis, and J\u00f6rg Siekmann. Reasoning with Assertions and Examples. Technical Report SEKI Report SR-93-10, Universit\u00e4t des Saarlandes, Fachbereich Informatik, 1993."},{"key":"57_CR9","doi-asserted-by":"crossref","unstructured":"D. Loveland. A Simplified Version for the Model Elimination Theorem Proving Procedure. JACM, 16(3), 1969.","DOI":"10.1145\/321526.321527"},{"key":"57_CR10","doi-asserted-by":"crossref","unstructured":"D.W. Loveland. Near-Horn Prolog. In J.-L. Lassez, editor, Proc. of the 4th Int. Conf. on Logic Programming, pages 456\u2013469. The MIT Press, 1987.","DOI":"10.21236\/ADA185172"},{"key":"57_CR11","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":"57_CR12","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"},{"key":"57_CR13","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"},{"key":"57_CR14","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP problem library. In Proc. CADE-12. Springer, 1994.","DOI":"10.1007\/3-540-58156-1_18"},{"key":"57_CR15","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":"57_CR16","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":"57_CR17","doi-asserted-by":"crossref","unstructured":"M. Stickel. A Prolog Technology Theorem Prover. In M.E. Stickel, editor, Proc CADE 10, LNCS 449, pages 673\u2013675. Springer, 1990.","DOI":"10.1007\/3-540-52885-7_136"}],"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_57","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T08:21:22Z","timestamp":1558254082000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_57"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_57","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"}}]}}