{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:53Z","timestamp":1749182813530,"version":"3.41.0"},"reference-count":27,"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:1005890730317","type":"journal-article","created":{"date-parts":[[2002,12,21]],"date-time":"2002-12-21T23:56:21Z","timestamp":1040514981000},"page":"173-203","source":"Crossref","is-referenced-by-count":0,"title":["Structuring Resolution Proofs by Introducing New Lemmata"],"prefix":"10.1007","volume":"19","author":[{"given":"K.","family":"H\u00f6rwein","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"135378_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. B. Andrews","year":"1981","unstructured":"Andrews, P. B.: Theorem proving via general matings, J. ACM\n28(1981), 193\u2013214.","journal-title":"J. ACM"},{"key":"135378_CR2","first-page":"287","volume":"194","author":"M. Baaz","year":"1985","unstructured":"Baaz, M. and Leitsch, A.: Die Anwendung starker Reduktionsregeln in automatischen Beweisen, Proc. Austrian Acad. Sci. II\n194(1985), 287\u2013307.","journal-title":"Proc. Austrian Acad. Sci. II"},{"key":"135378_CR3","first-page":"30","volume-title":"Proc. ISSAC\u201990","author":"M. Baaz","year":"1991","unstructured":"Baaz, M. and Leitsch, A.: A strong problem reduction method based on function introduction, in Proc. ISSAC\u201990, ACM Press, New York, Addison-Wesley, Reading, MA, 1991, pp. 30\u201337."},{"key":"135378_CR4","doi-asserted-by":"crossref","unstructured":"Baaz, M. and Leitsch, A.: Complexity of Resolution Proofs and Function Introduction, Ann. Pure Appl. Logic 57, North-Holland, Amsterdam, 1992, pp. 181\u2013215.","DOI":"10.1016\/0168-0072(92)90042-X"},{"key":"135378_CR5","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1994-2044","volume":"20","author":"M. Baaz","year":"1992","unstructured":"Baaz, M. and Leitsch, A.: On Skolemization and proof complexity, Fundamenta Informaticae\n20(1992), 353\u2013379.","journal-title":"Fundamenta Informaticae"},{"key":"135378_CR6","doi-asserted-by":"crossref","first-page":"844","DOI":"10.1145\/182.183","volume":"26","author":"W. Bibel","year":"1983","unstructured":"Bibel, W.: Matings in matrices, Comm. ACM\n26(1983), 844\u2013852.","journal-title":"Comm. ACM"},{"key":"135378_CR7","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Automated Theorem Proving, Vieweg, Braunschweig, 2nd edition, 1987.","DOI":"10.1007\/978-3-322-90102-6"},{"key":"135378_CR8","volume-title":"Deduction: Automated Logic","author":"W. Bibel","year":"1993","unstructured":"Bibel, W.: Deduction: Automated Logic, Academic Press, London, 1993."},{"key":"135378_CR9","unstructured":"Eder, E.: An implementation of a theorem prover based on the connection method, in AIMSA 84, North-Holland, Amsterdam, 1984."},{"key":"135378_CR10","doi-asserted-by":"crossref","unstructured":"Eder, E.: Relative Complexities of First Order Calculi, Vieweg, Wiesbaden, Germany, 1992.","DOI":"10.1007\/978-3-322-84222-0"},{"key":"135378_CR11","first-page":"148","volume-title":"LPAR\u201992, LNAI 624","author":"U. Egly","year":"1992","unstructured":"Egly, U.: Shortening proofs by quantifier introduction, in LPAR\u201992, LNAI 624, Springer, Berlin, 1992, pp. 148\u2013159."},{"key":"135378_CR12","first-page":"172","volume-title":"KGC\u201993, LNCS 713","author":"U. Egly","year":"1993","unstructured":"Egly, U.: On different concepts of function introduction, in KGC\u201993, LNCS 713, Springer, Berlin, 1993, pp. 172\u2013183."},{"key":"135378_CR13","unstructured":"Egly, U.: On Methods of Function Introduction and Related Concepts, Dissertation, Technische Hochschule Darmstadt, 1994."},{"key":"135378_CR14","doi-asserted-by":"crossref","unstructured":"Eisinger, N., Ohlbach, H. J. and Pr\u00e4cklein, A.: Reduction rules for resolution-based systems, Artificial Intelligence\n50(1991).","DOI":"10.1016\/0004-3702(91)90098-5"},{"key":"135378_CR15","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1934","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen I\u2013II, Math. Z.\n39(1934), 176\u2013210, 405\u2013431, reprinted in Gerhard Gentzen, The Collected Papers of Gerhard GentzenM. E. Szabo (ed.), North-Holland, Amsterdam, 1969.","journal-title":"Math. Z."},{"key":"135378_CR16","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1016\/0004-3702(93)90069-N","volume":"61","author":"G. Gottlob","year":"1993","unstructured":"Gottlob, G. and Ferm\u00fcller, Ch.: Removing redundancy from a clause, Artificial Intelligence\n61(1993), 263\u2013289.","journal-title":"Artificial Intelligence"},{"key":"135378_CR17","doi-asserted-by":"crossref","unstructured":"Gottlob, G. and Leitsch, A.: On the efficiency of subsumption algorithms, J. ACM\n32(2)(1985).","DOI":"10.1145\/3149.214118"},{"key":"135378_CR18","doi-asserted-by":"crossref","first-page":"398","DOI":"10.1145\/321958.321960","volume":"23","author":"W. H. Joyner","year":"1978","unstructured":"Joyner, W. H.: Resolution strategies as decision procedures, J. ACM\n23(1978), 398\u2013417.","journal-title":"J. ACM"},{"key":"135378_CR19","first-page":"25","volume":"9","author":"S.-J. Lee","year":"1992","unstructured":"Lee, S.-J. and Plaisted, D. A.: Eliminating duplication with the hyper-linking strategy, J. Automated Reasoning\n9(1992), 25\u201342.","journal-title":"J. Automated Reasoning"},{"key":"135378_CR20","series-title":"Technical report","volume-title":"OTTER, 2.0 Users Guide","author":"W. W. McCune","year":"1990","unstructured":"McCune, W. W.: OTTER, 2.0 Users Guide, Technical report ANL-90\/9, Argonne National Laboratory, Argonne, IL, 1990."},{"key":"135378_CR21","first-page":"365","volume-title":"CADE-8, LNCS 230","author":"D. A. Plaisted","year":"1986","unstructured":"Plaisted, D. A.: Abstraction using generalization functions, in CADE-8, LNCS 230, Springer, Berlin, 1986, pp. 365\u2013376."},{"key":"135378_CR22","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. A. Plaisted","year":"1986","unstructured":"Plaisted, D. A. and Greenbaum, S.: A structure preserving clause form translation, J. Symbolic Computation\n2(1986), 293\u2013304.","journal-title":"J. Symbolic Computation"},{"key":"135378_CR23","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1145\/321021.321023","volume":"7","author":"D. Prawitz","year":"1960","unstructured":"Prawitz, D., Prawitz, H. and Voghera, N.: A mechanical proof procedure and its realization in an electronic computer, J. ACM\n7(1960), 102\u2013128.","journal-title":"J. ACM"},{"key":"135378_CR24","first-page":"59","volume":"4","author":"D. Prawitz","year":"1969","unstructured":"Prawitz, D.: Advances and problems in mechanical proof procedures, Mach. Intell.\n4(1969), 59\u201371.","journal-title":"Mach. Intell."},{"issue":"1","key":"135378_CR25","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"Robinson, J. A.: A machine-oriented logic based on the resolution principle, J. ACM\n12(1) (1965), 23\u201341.","journal-title":"J. ACM"},{"key":"135378_CR26","first-page":"1","volume-title":"CADE-12, LNAI 814","author":"J. Slaney","year":"1994","unstructured":"Slaney, J.: The crisis in finite mathematics: automated reasoning as cause and cure, in CADE-12, LNAI 814, Springer, Berlin, 1994, pp. 1\u201313."},{"key":"135378_CR27","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning","author":"G. S. Tseitin","year":"1983","unstructured":"Tseitin, G. S.: On the complexity of derivation in propositional calculus, Automation of Reasoning, J. Siekmann and G. Wrightson (eds), Springer, Berlin, 1983, pp. 466\u2013483."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005890730317.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1005890730317\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1005890730317.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:40:08Z","timestamp":1749123608000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1005890730317"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997,10]]},"references-count":27,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1997,10]]}},"alternative-id":["135378"],"URL":"https:\/\/doi.org\/10.1023\/a:1005890730317","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[1997,10]]}}}