{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:40:04Z","timestamp":1749123604117,"version":"3.41.0"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1997,10,1]],"date-time":"1997-10-01T00:00:00Z","timestamp":875664000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1997,10,1]],"date-time":"1997-10-01T00:00:00Z","timestamp":875664000000},"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":[[1997,10]]},"DOI":"10.1023\/a:1005812703468","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T23:56:21Z","timestamp":1040514981000},"page":"205-262","source":"Crossref","is-referenced-by-count":5,"title":["A Disjunctive Positive Refinement of Model Elimination and its Application to Subsumption Deletion"],"prefix":"10.1007","volume":"19","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Br\u00fcning","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"139899_CR1","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1093\/jigpal\/2.2.229","volume":"2","author":"G. Antoniou","year":"1994","unstructured":"Antoniou, G. and Langetepe, E.: Applying SLD-resolution to a class of non-Horn logic programs, Bulletin of the IGPL\n2(2) (1994), 231\u2013243.","journal-title":"Bulletin of the IGPL"},{"key":"139899_CR2","doi-asserted-by":"crossref","unstructured":"Astrachan, O. L. and Stickel, M. E.: Caching and lemmaizing in model elimination theorem provers, in D. Kapur (ed.), Proc. Conf. Automated Deduction, Vol. 607 Lecture Notes in Artificial Intelligence, Springer, 1992, pp. 224\u2013238.","DOI":"10.1007\/3-540-55602-8_168"},{"key":"139899_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-7118-2","volume-title":"Canonical Equational Proofs","author":"L. Bachmair","year":"1991","unstructured":"Bachmair, L.: Canonical Equational Proofs, Progress in Theoretical Computer Science, Birkh\u00e4user, 1991."},{"key":"139899_CR4","unstructured":"Baumgartner, P.: Refinements of theory model elimination and a variant without contrapositives, in A. G. Cohn (ed.), 11th European Conference on Artificial Intelligence, ECAI 94, Wiley, 1994. (Long version in: Research Report 8\/93, University of Koblenz, Institute for Computer Science, Koblenz, Germany)."},{"issue":"3","key":"139899_CR5","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/BF00252179","volume":"16","author":"P. Baumgartner","year":"1996","unstructured":"Baumgartner, P.: Linear and unit-resulting refutations for Horn theories, J. Automated Reasoning\n16(3) (1996), 241\u2013319.","journal-title":"J. Automated Reasoning"},{"key":"139899_CR6","doi-asserted-by":"crossref","unstructured":"Baumgartner, P. and Furbach, U.: Consolution as a framework for comparing calculi, J. Symbolic Computation\n16(5) (1993).","DOI":"10.1006\/jsco.1993.1058"},{"key":"139899_CR7","doi-asserted-by":"crossref","first-page":"339","DOI":"10.1007\/BF00881948","volume":"13","author":"P. Baumgartner","year":"1994","unstructured":"Baumgartner, P. and Furbach, U.: Model elimination without contrapositives and its application to PTTP, J. Automated Reasoning\n13(1994), 339\u2013359. Short version in: Proceedings of CADE-12, Springer LNAI 814, 1994, pp. 87\u2013101.","journal-title":"J. Automated Reasoning"},{"key":"139899_CR8","doi-asserted-by":"crossref","unstructured":"Baumgartner, P. and Furbach, U.: PROTEIN: A PROver with a Theory Extension Interface, in A. Bundy (ed.), Automated Deduction\u2013CADE-12, Vol. 814 Lecture Notes in Artificial Intelligence, Springer, 1994, pp. 769\u2013773. Available on the WWW, URL http:\/\/www.uni-koblenz.de\/ag-ki\/Systems\/PROTEIN\/.","DOI":"10.1007\/3-540-58156-1_57"},{"key":"139899_CR9","unstructured":"Baumgartner, P., Furbach, U. and Stolzenburg, F.: Model elimination, logic programming and computing answers, in 14th Int. Joint Conference on Artificial Intelligence (IJCAI 95), Vol. 1, 1995. (Long version in Research Report 1\/95, University of Koblenz, Germany. To appear in Artificial Intelligence)."},{"key":"139899_CR10","series-title":"Technical Report","volume-title":"On Infinite Loops in Logic Programming","author":"P. Besnard","year":"1989","unstructured":"Besnard, P.: On Infinite Loops in Logic Programming, Technical Report 488, IRISA, Rennes, France, 1989."},{"issue":"3","key":"139899_CR11","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/0167-739X(85)90019-6","volume":"1","author":"W. Bibel","year":"1985","unstructured":"Bibel, W. and Buchberger, B.: Towards a connection machine for logical inference, Future Generations Computer Systems Journal\n1(3) (1985), 177\u2013188.","journal-title":"Future Generations Computer Systems Journal"},{"key":"139899_CR12","first-page":"511","volume-title":"International Joint Conference on Artificial Intelligence","author":"Bl\u00e4sius K","year":"1981","unstructured":"Bl\u00e4sius, K., Eisinger, N., Siekmann, J., Smolka, G., Herold, A. and Walther, C.: The Markgraf Karl refutation procedure, in International Joint Conference on Artificial Intelligence, Los Altos, CA. Morgan Kaufmann, 1981, pp. 511\u2013518."},{"key":"139899_CR13","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0304-3975(91)90004-L","volume":"86","author":"R. N. Bol","year":"1991","unstructured":"Bol, R. N., Apt, K. R. and Klop, J. W.: An analysis of loop checking mechanisms for logic programming, J. Theoret. Computer Science\n86(1991), 35\u201379.","journal-title":"J. Theoret. Computer Science"},{"key":"139899_CR14","unstructured":"Br\u00fcning, S.: On loop detection in connection calculi, in G. Gottlob, A. Leitsch, and D. Mundici (eds), Proc. Kurt G\u00f6del Colloquium, Springer, 1993, pp. 144\u2013151."},{"key":"139899_CR15","unstructured":"Br\u00fcning, S.: Techniques for avoiding redundancy in theorem proving based on the connection method, PhD Thesis, TH Darmstadt, 1994."},{"key":"139899_CR16","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. L. Chang","year":"1973","unstructured":"Chang, C. L. and Lee, R. C.-T: Symbolic Logic and Mechanical Theorem Proving, Academic Press, New York, 1973."},{"key":"139899_CR17","unstructured":"Fronh\u00f6fer, B.: On refinements of the connection method, in J. Demetrovics, G. Katona, and A. Salomaa (eds), Algebra, Combinatorics and Logic in Computer Science, North Holland, 1985, pp. 391\u2013401."},{"key":"139899_CR18","unstructured":"Fronh\u00f6fer, B. and Caferra, R.: Memorization of literals: An enhancement of the connection method, Technical report, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen, 1988."},{"key":"139899_CR19","unstructured":"Gallier, J.: Logic for Computer Science: Foundations of Automatic Theorem Proving, Wiley, 1987."},{"key":"139899_CR20","doi-asserted-by":"crossref","unstructured":"Graf, P.: Extended path-indexing, in Automated Deduction\u2013CADE 12, Vol. 814 Lecture Notes in Artifical Intelligence, Springer, 1994.","DOI":"10.1007\/3-540-58156-1_37"},{"key":"139899_CR21","unstructured":"Letz, R.: First-order calculi and proof procedures for automated deduction, PhD Thesis, TH Darmstadt, 1993."},{"issue":"3","key":"139899_CR22","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"Letz, R., Mayr, K. and Goller, Ch.: Controlled integrations of the cut rule into connection tableau calculi, J. Automated Reasoning\n13(3) (1994), 297\u2013338. Special Issue on Automated Reasoning with Analytic Tableaux.","journal-title":"J. Automated Reasoning"},{"issue":"2","key":"139899_CR23","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, J. Automated Reasoning\n8(2) (1992), 183\u2013212.","journal-title":"J. Automated Reasoning"},{"key":"139899_CR24","doi-asserted-by":"crossref","unstructured":"Lloyd, J. W: Foundations of Logic Programming, 2nd edition, Springer, 1987.","DOI":"10.1007\/978-3-642-83189-8"},{"key":"139899_CR25","doi-asserted-by":"crossref","unstructured":"Loveland, D.: Mechanical theorem proving by model elimination, JACM\n15(2) (1968).","DOI":"10.1145\/321450.321456"},{"key":"139899_CR26","unstructured":"Loveland, D.: Automated Theorem Proving-A Logical Basis, North Holland, 1978."},{"key":"139899_CR27","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D. W. Loveland","year":"1986","unstructured":"Loveland, D. W.: Mechanical theorem proving by model elimination, J. ACM\n15(1986), 236\u2013251.","journal-title":"J. ACM"},{"key":"139899_CR28","doi-asserted-by":"crossref","unstructured":"Loveland, D. W. and Reed, D. W.: Near-Horn Prolog and the ancestry family of proof procedures, Annals of Mathematics and Artificial Intelligence\n14(1995).","DOI":"10.1007\/BF01530821"},{"key":"139899_CR29","doi-asserted-by":"crossref","unstructured":"Mayr, K.: Link deletion in model elimination, in R. H\u00e4hnle, P. Baumgartner and J. Posegga (eds), Theorem Proving with Analytic Tableaux and Related Methods, Vol. 918 Lecture Notes in Artificial Intelligence, Springer, 1995, pp. 169\u2013184.","DOI":"10.1007\/3-540-59338-1_35"},{"key":"139899_CR30","series-title":"Technical Report","volume-title":"From Horn clauses to first order logic: A graceful ascent","author":"G. Neugebauer","year":"1992","unstructured":"Neugebauer, G.: From Horn clauses to first order logic: A graceful ascent, Technical Report AIDA\u201392\u201321, FG Intellektik, FB Informatik, TH Darmstadt, 1992."},{"key":"139899_CR31","unstructured":"Overbeek, R. and Wos, L.: Subsumption, a sometimes undervalued procedure, in J.-L. Lassez and G. Plotkin (eds), Festschrift for J. A. Robinson,MIT Press, 1991, pp. 3\u201340."},{"issue":"6","key":"139899_CR32","first-page":"389","volume":"4","author":"D. Plaisted","year":"1990","unstructured":"Plaisted, D.: A sequent-style model elimination strategy and a positive refinement, J. Automated Reasoning\n4(6) (1990), 389\u2013402.","journal-title":"J. Automated Reasoning"},{"issue":"8","key":"139899_CR33","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1145\/988346.988350","volume":"20","author":"D. Poole","year":"1985","unstructured":"Poole, D. and Goebel, R.: On eliminating loops in Prolog, Sigplan Notices\n20(8) (1985), 38\u201340.","journal-title":"Sigplan Notices"},{"issue":"1","key":"139899_CR34","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, J. Logic Programming\n12(1) (1992), 25\u201350.","journal-title":"J. Logic Programming"},{"key":"139899_CR35","unstructured":"Robinson, G. A. and Wos, L.: Paramodulation and theorem proving in first-order theories with equality, in R. Meltzer and D. Mitchie (eds), Machine Intelligence 4, Edinburgh University Press, 1969, pp. 135\u2013150."},{"key":"139899_CR36","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF01530763","volume":"12","author":"B. Spencer","year":"1994","unstructured":"Spencer, B.: Avoiding duplicate proofs with the foothold refinement, Annals of Math. and Artificial Intelligence\n12(1994), 117\u2013140.","journal-title":"Annals of Math. and Artificial Intelligence"},{"issue":"4","key":"139899_CR37","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/BF03037328","volume":"2","author":"M. E. Stickel","year":"1984","unstructured":"Stickel, M. E.: A Prolog technology theorem prover, New Generation Computing\n2(4) (1984), 371\u2013383.","journal-title":"New Generation Computing"},{"key":"139899_CR38","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, J. Automated Reasoning\n4(1988), 353\u2013380.","journal-title":"J. Automated Reasoning"},{"key":"139899_CR39","unstructured":"Sutcliffe, G.: A linear deduction system with integrated semantic guidance, PhD Thesis, University of Western Australia, 1992."},{"key":"139899_CR40","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G.: Linear-input subset analysis, in D. Kapur (ed.), Proceedings of the Conference on Automated Deduction, Springer, 1992, pp. 268\u2013280.","DOI":"10.1007\/3-540-55602-8_171"},{"key":"139899_CR41","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Suttner, Ch. and Yemenis, T.: The TPTP problem library, in A. Bundy (ed.), Proc. Conf. on Automated Deduction, Vol. 814 Lecture Notes in Artificial Intelligence, Springer, 1994, pp. 252\u2013266.","DOI":"10.1007\/3-540-58156-1_18"},{"key":"139899_CR42","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0167-739X(93)90002-7","volume":"9","author":"R. P. van de Riet","year":"1993","unstructured":"van de Riet, R. P.: An overview and appraisal of the fifth generation computer system project, Future Generation Computer Systems Journal\n9(1993), 83\u2013103.","journal-title":"Future Generation Computer Systems Journal"},{"key":"139899_CR43","doi-asserted-by":"crossref","unstructured":"Wos, L., Winker, S., McCune, W., Overbeek, R., Lusk, E. and Stevens, R.: Automated reasoning contributes to mathematics and logic, in M. E. Stickel (ed.), Proc. Conf. on Automated Deduction, Springer, 1990, pp. 485\u2013499.","DOI":"10.1007\/3-540-52885-7_109"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005812703468.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005812703468\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005812703468.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:23:48Z","timestamp":1749122628000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005812703468"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,10]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1997,10]]}},"alternative-id":["139899"],"URL":"https:\/\/doi.org\/10.1023\/a:1005812703468","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1997,10]]}}}