{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:47:30Z","timestamp":1749124050283},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"3","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":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/bf00881948","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T19:25:12Z","timestamp":1104002712000},"page":"339-359","source":"Crossref","is-referenced-by-count":22,"title":["Model elimination without contrapositives and its application to PTTP"],"prefix":"10.1007","volume":"13","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ulrich","family":"Furbach","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"Astrachan, Owen L. and Stickel, Mark E.: Caching and lemmaizing in model elimination theorem provers, in D. Kapur (ed.),Proc. 11th International Conference on Automated Deduction (CADE-11), Springer-Verlag, LNAI 607, 1992, pp. 224?238.","DOI":"10.1007\/3-540-55602-8_168"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Baumgartner, P. and Furbach, U.: Consolution as a framework for comparing calculi,Journal of Symbolic Computation 16(5) (1993).","DOI":"10.1006\/jsco.1993.1058"},{"key":"CR3","doi-asserted-by":"crossref","unstructured":"Baumgartner, P. and Furbach, U.: PROTEIN: APROver with aTheoryExtension\/Interface, in A. Bundy (ed.),Proc. 12th International Conference on Automated Deduction (CADE-12), Lecture Notes in AI 814, Springer-Verlag, 1994, pp. 769?773.","DOI":"10.1007\/3-540-58156-1_57"},{"key":"CR4","doi-asserted-by":"crossref","unstructured":"Baumgartner, P.: A model elimination calculus with built-in theories, in H.-J. Ohlbach (ed.),Proc. 16-th German AI-Conference (GWAI-92), Lecture Notes in AI 671, Springer-Verlag, 1992, pp. 30?42.","DOI":"10.1007\/BFb0018990"},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"Bibel, W.:Automated Theorem Proving, Vieweg, 2nd edn, 1987.","DOI":"10.1007\/978-3-322-90102-6"},{"key":"CR6","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/BF00244493","volume":"6","author":"W. W. Bledsoe","year":"1990","unstructured":"Bledsoe, W. W.: Challenge problems in elementary calculus,Journal of Automated Reasoning 6 (1990), 341?359.","journal-title":"Journal of Automated Reasoning"},{"key":"CR7","unstructured":"Chang, C. and Lee, R.:Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973."},{"key":"CR8","unstructured":"Eder, E.: Consolution and Its Relation with Resolution, inProc. IJCAI'91, 1991."},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"Eder, E.:Relative Complexities of First Order Languages, Vieweg, 1992.","DOI":"10.1007\/978-3-322-84222-0"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"Fitting, M.:First-Order Logic and Automated Theorem Proving, Texts and Monographs in Computer Science, Springer, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"issue":"4","key":"CR11","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1016\/S0743-1066(85)80003-0","volume":"2","author":"D. M. Gabbay","year":"1985","unstructured":"Gabbay, D. M.: N-Prolog: An extension of Prolog with hypothetical implication II. Logical foundations, and negation as failure,Journal of Logic Programming 2(4) (1985), 251?284.","journal-title":"Journal of Logic Programming"},{"key":"CR12","unstructured":"Gallier, J.:Logic for Computer Science: Foundations of Automatic Theorem Proving, Wiley, 1987."},{"issue":"2","key":"CR13","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S., and Bibel, W.: SETHEO: A high-performance theorem prover,Journal of Automated Reasoning 8(2) (1992), 183?212.","journal-title":"Journal of Automated Reasoning"},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"Lloyd, J.:Foundations of Logic Programming, Symbolic Computation. Springer, second, extended edition, 1987.","DOI":"10.1007\/978-3-642-83189-8"},{"key":"CR15","unstructured":"Loveland, D. W. and Reed, D. W.:A Near-Horn Prolog for Compilation, Technical Report CS-1989-14, Duke University, 1989."},{"key":"CR16","doi-asserted-by":"crossref","unstructured":"Loveland, D.: Mechanical theorem proving by model elimination,JACM 15(2) (1968).","DOI":"10.1145\/321450.321456"},{"key":"CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/BF00249353","volume":"7","author":"D. Loveland","year":"1991","unstructured":"Loveland, D.: Near-Horn Prolog and beyond,Journal of Automated Reasoning 7 (1991), 1?26.","journal-title":"Journal of Automated Reasoning"},{"key":"CR18","volume-title":"Proc. 9th CADE","author":"R. Manthey","year":"1988","unstructured":"Manthey, R. and Bry, F.: SATCHMO: A theorem prover implemented in Prolog, inProc. 9th CADE, Illinois, Springer LNCS, 1988."},{"key":"CR19","unstructured":"Mellouli, Ta?eb: A Tree Representation of the Modified Problem Reduction and Its Extension to Three-valued Logic. KI-NRW 90-19, Universit\ufffdt Duisburg, FB 11 ? Praktische Informatik, 1990."},{"key":"CR20","volume-title":"Jos\ufffd:SLWV ? A Theorem Prover for Logic Programming","author":"Luis Pereira","year":"1991","unstructured":"Pereira, Luis, Moniz, Caires, Luis, and Alferes, Jos\ufffd:SLWV ? A Theorem Prover for Logic Programming, AI Centre, Uninova, Monte da Caparica, Portugal, 1991."},{"key":"CR21","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244944","volume":"4","author":"D. Plaisted","year":"1988","unstructured":"Plaisted, D.: Non-Horn clause logic programming without contrapositives,Journal of Automated Reasoning 4 (1988), 287?325.","journal-title":"Journal of Automated Reasoning"},{"issue":"6","key":"CR22","first-page":"389","volume":"4","author":"D. Plaisted","year":"1990","unstructured":"Plaisted, D.: A sequent-style model elimination strategy and a positive refinement,Journal of Automated Reasoning 4(6) (1990), 389?402.","journal-title":"Journal of Automated Reasoning"},{"key":"CR23","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1016\/0743-1066(92)90038-5","volume":"12","author":"D. W. Reed","year":"1992","unstructured":"Reed, D. W. and Loveland, D. W.: A comparison of three Prolog extensions,Journal of Logic Programming 12 (1992), 25?50.","journal-title":"Journal of Logic Programming"},{"key":"CR24","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. Stickel","year":"1988","unstructured":"Stickel, M.: A Prolog technology theorem prover: Implementation by an extended Prolog compiler,Journal of Automated Reasoning 4 (1988), 353?380.","journal-title":"Journal of Automated Reasoning"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"Stickel, M.: A Prolog technology theorem prover: A new exposition and implementation in Prolog. Technical note 464, SRI International, 1989.","DOI":"10.1007\/3-540-52531-9_135"},{"key":"CR26","unstructured":"Wos, L.:Automated Reasoning: 33 Basic Research Problems, Prentice-Hall, 1988."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881948.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881948\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881948","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,1]],"date-time":"2023-05-01T03:28:17Z","timestamp":1682911697000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881948"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1994]]}},"alternative-id":["BF00881948"],"URL":"https:\/\/doi.org\/10.1007\/bf00881948","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}