{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:46Z","timestamp":1761611146334},"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\/bf00881947","type":"journal-article","created":{"date-parts":[[2004,12,25]],"date-time":"2004-12-25T19:25:12Z","timestamp":1104002712000},"page":"297-337","source":"Crossref","is-referenced-by-count":118,"title":["Controlled integration of the cut rule into connection tableau calculi"],"prefix":"10.1007","volume":"13","author":[{"given":"R.","family":"Letz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K.","family":"Mayr","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C.","family":"Goller","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","unstructured":"Astrachan, O. W. and Loveland, D. W.: METEORs: High performance theorem provers using model elimination, in R. S. Boyer (ed.),Automated Reasoning: Essays in Honour of Woody Bledsoe, Kluwer Academic Publishers, 1991.","DOI":"10.1007\/978-94-011-3488-0_2"},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Astrachan, O. W. and Stickel, M. E.: Caching and lemmaizing in model elimination theorem provers,Proc. 11th Conference on Automated Deduction (CADE-11), Saratoga Springs, Lecture Notes in AI 607, Springer, 1992, pp. 224?238.","DOI":"10.1007\/3-540-55602-8_168"},{"key":"CR3","volume-title":"The Foundations of Mathematics","author":"E. W. Beth","year":"1959","unstructured":"Beth, E. W.:The Foundations of Mathematics, North-Holland, Amsterdam, 1959."},{"issue":"13","key":"CR4","first-page":"309","volume":"18","author":"E. W. Beth","year":"1955","unstructured":"Beth, E. W.: Semantic entailment and formal derivability,Mededlingen der Koninklijke Nederlandse Akademie van Wetenschappen 18(13) (1955), 309?342.","journal-title":"Mededlingen der Koninklijke Nederlandse Akademie van Wetenschappen"},{"key":"CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-322-90102-6","volume-title":"Automated Theorem Proving","author":"W. Bibel","year":"1987","unstructured":"Bibel, W.:Automated Theorem Proving, 2nd edn, Vieweg Verlag, Braunschweig, 1987.","edition":"2nd edn"},{"key":"CR6","doi-asserted-by":"crossref","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"Bibel, W.: On matrices with connections,J. ACM 28 (1981) 633?645.","journal-title":"J. ACM"},{"key":"CR7","unstructured":"Eder, E.: Consolution and its relation with resolution.Proc. 12th International Joint Conference on Artificial Intelligence (IJCAI-91), Sydney, Morgan Kaufmann, 1991, pp. 132?136."},{"key":"CR8","doi-asserted-by":"crossref","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \ufffdber das logische Schlie\ufffden,Mathematische Zeitschrift 39 (1935), 176?210 and 405?431.","journal-title":"Mathematische Zeitschrift"},{"key":"CR9","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0004-3702(85)90084-0","volume":"27","author":"R. E. Korf","year":"1985","unstructured":"Korf, R. E.: Depth-first iterative deepening: an optimal admissible tree search,Artificial Intelligence 27 (1985), 97?109.","journal-title":"Artificial Intelligence"},{"key":"CR10","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","volume":"2","author":"R. A. Kowalski","year":"1971","unstructured":"Kowalski, R. A. and Kuehner, D.: Linear resolution with selection function,Artificial Intelligence 2 (1971), 227?260.","journal-title":"Artificial Intelligence"},{"key":"CR11","unstructured":"Letz, R.: First-Order Calculi and Proof Procedures for Automated Deduction, PhD thesis. Technische Hochschule Darmstadt, 1993."},{"key":"CR12","unstructured":"Letz, R.: Polynomial Simulation of Sequent Systems by Tree Sequent Systems. Technical report, Technische Universit\ufffdt M\ufffdnchen, 1993."},{"key":"CR13","unstructured":"Letz, R. and Mayr, K.:The Relation of Extended Tableau Systems with Semantic Trees and Linear Resolution, Technical report, Technische Universit\ufffdt M\ufffdnchen, 1994."},{"issue":"2","key":"CR14","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 8(2) (1992), 183?212.","journal-title":"J. Automated Reasoning"},{"key":"CR15","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D. W. Loveland","year":"1978","unstructured":"Loveland, D. W.:Automated Theorem Proving: A Logical Basis, North-Holland, Amsterdam, 1978."},{"issue":"2","key":"CR16","doi-asserted-by":"crossref","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D. W. Loveland","year":"1968","unstructured":"Loveland, D. W.: Mechanical theorem proving by model elimination,J. ACM 15(2) (1968), 236?251.","journal-title":"J. ACM"},{"key":"CR17","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1145\/321526.321527","volume":"16","author":"D. W. Loveland","year":"1969","unstructured":"Loveland, D. W.: A simplified format for the model elimination theorem-proving procedure,J. ACM 16 (1969), 349?363.","journal-title":"J. ACM"},{"key":"CR18","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1145\/321694.321706","volume":"19","author":"D. W. Loveland","year":"1972","unstructured":"Loveland, D. W.: A unifying view of some linear Herbrand procedures,J. ACM 19 (1972), 366?384.","journal-title":"J. ACM"},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"Mayr, K.: Refinements and extensions of model elimination.Proc. 4th International Conference on Logic Programming and Automated Reasoning (LPAR'93), St. Petersburg, Lecture Notes in AI 698, Springer-Verlag, 1993, pp. 217?228.","DOI":"10.1007\/3-540-56944-8_55"},{"key":"CR20","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","volume":"26","author":"D. Prawitz","year":"1960","unstructured":"Prawitz, D.: An improved proof procedure,Theoria 26 (1960), 102?139.","journal-title":"Theoria"},{"key":"CR21","unstructured":"Reckhow, R. A.: On the Lengths of Proofs in the Propositional Calculus, PhD thesis, University of Toronto, 1976."},{"key":"CR22","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1016\/0004-3702(76)90021-7","volume":"7","author":"R. E. Shostak","year":"1976","unstructured":"Shostak, R. E.: Refutation graphs,Artificial Intelligence 7 (1976), 51?64.","journal-title":"Artificial Intelligence"},{"key":"CR23","doi-asserted-by":"crossref","unstructured":"Smullyan, R. M.:First Order Logic, Springer-Verlag, 1968.","DOI":"10.1007\/978-3-642-86718-7"},{"key":"CR24","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. A. Stickel","year":"1988","unstructured":"Stickel, M. A.: A Prolog technology theorem prover: implementation by an extended Prolog compiler,J. Automated Reasoning 4 (1988), 353?380.","journal-title":"J. Automated Reasoning"},{"key":"CR25","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., Suttner, C. B., and Yemenis, T.: The TPTP problem library.Proc. 12th International Conference on Automated Deduction, 1994.","DOI":"10.1007\/3-540-58156-1_18"},{"key":"CR26","doi-asserted-by":"crossref","first-page":"782","DOI":"10.1109\/TC.1976.1674697","volume":"C-25","author":"G. A. Wilson","year":"1976","unstructured":"Wilson, G. A. and Minker, J.: Resolution, refinements, and search strategies: a comparative study,IEEE Trans. Computers C-25 (1976), 782?801.","journal-title":"IEEE Trans. Computers"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881947.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881947\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881947","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T12:58:12Z","timestamp":1556542692000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881947"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"references-count":26,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1994]]}},"alternative-id":["BF00881947"],"URL":"https:\/\/doi.org\/10.1007\/bf00881947","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}