{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:14:51Z","timestamp":1725664491840},"publisher-location":"Berlin, Heidelberg","reference-count":61,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540593386"},{"type":"electronic","value":"9783540492351"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59338-1_24","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T12:13:32Z","timestamp":1330258412000},"page":"1-16","source":"Crossref","is-referenced-by-count":3,"title":["Issues in theorem proving based on the connection method"],"prefix":"10.1007","author":[{"given":"W.","family":"Bibel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Br\u00fcning","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"U.","family":"Egly","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"Korn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T.","family":"Rath","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"1_CR1","first-page":"414","volume":"36","author":"P. B. Andrews","year":"1971","unstructured":"P. B. Andrews. Resolution in Type Theory. JSL, 36:414\u2013432, 1971.","journal-title":"JSL"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"O. L. Astrachan and M. E. Stickel. Caching and Lemmaizing in Model Elimination Theorem Provers. In D. Kapur, editor, Proceedings of CADE, volume 607 of LNAI, pages 224\u2013238. Springer, 1992.","DOI":"10.1007\/3-540-55602-8_168"},{"key":"1_CR3","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1016\/0304-3975(79)90035-5","volume":"9","author":"R. Aubin","year":"1979","unstructured":"R. Aubin. Mechanizing structural induction. TCS, 9:347\u2013362, 1979.","journal-title":"TCS"},{"key":"1_CR4","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1994-2044","volume":"20","author":"M. Baaz","year":"1994","unstructured":"M. Baaz and A. Leitsch. On Skolemization and Proof Complexity. Fundamenta Informaticae, 20:353\u2013379, 1994.","journal-title":"Fundamenta Informaticae"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"L. Bachmair, H. Ganzinger, C. Lynch, and W. Snyder. Basic paramodulation and superposition. In D. Kapur, editor, Proceedings of CADE, volume 607 of LNAI, pages 462\u2013476. Springer Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_185"},{"key":"1_CR6","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/BF02239498","volume":"12","author":"W. Bibel","year":"1974","unstructured":"W. Bibel. An Approach to a Systematic Theorem Proving Procedure in First-Order Logic. Computing, 12:43\u201355, 1974.","journal-title":"Computing"},{"issue":"4","key":"1_CR7","doi-asserted-by":"publisher","first-page":"633","DOI":"10.1145\/322276.322277","volume":"28","author":"W. Bibel","year":"1981","unstructured":"W. Bibel. On Matrices with Connections. JACM, 28(4):633\u2013645, 1981.","journal-title":"JACM"},{"key":"1_CR8","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/BF03037438","volume":"4","author":"W. Bibel","year":"1986","unstructured":"W. Bibel. A deductive solution for plan generation. New Generation Computing, 4:115\u2013132, 1986.","journal-title":"New Generation Computing"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg Verlag, 1987. Second edition.","DOI":"10.1007\/978-3-322-90102-6"},{"key":"1_CR10","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/3-540-50676-4_9","volume-title":"Advanced Topics in Artificial Intelligence","author":"W. Bibel","year":"1988","unstructured":"W. Bibel. Advanced topics in automated deduction. In R. Nossum, editor, Advanced Topics in Artificial Intelligence, pages 41\u201359, Berlin, 1988. Springer, LNCS 345."},{"key":"1_CR11","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF00244489","volume":"6","author":"W. Bibel","year":"1990","unstructured":"W. Bibel. Short proofs of the pigeonhole formulas based on the connection method. JAR, 6:287\u2013297, 1990.","journal-title":"JAR"},{"key":"1_CR12","volume-title":"Deduction: Automated Logic","author":"W. Bibel","year":"1993","unstructured":"W. Bibel. Deduction: Automated Logic. Academic Press, London, 1993."},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"W. Bibel, S. Br\u00fcning, U. Egly, and T. Rath. Komet. In A. Bundy, editor, Proceedings of CADE, number 814 in LNAI, pages 783\u2013787. Springer Verlag, 1994. System description.","DOI":"10.1007\/3-540-58156-1_60"},{"issue":"3","key":"1_CR14","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/0167-739X(85)90019-6","volume":"1","author":"W. Bibel","year":"1985","unstructured":"W. Bibel and B. Buchberger. Towards a connection machine for logical inference. Future Generations Computer Systems Journal, 1(3):177\u2013188, 1985.","journal-title":"Future Generations Computer Systems Journal"},{"key":"1_CR15","unstructured":"W. Bibel and E. Eder. Decomposition of tautologies into regular formulas and strong completeness of connection-graph resolution. JACM, submitted, 1994."},{"key":"1_CR16","first-page":"94","volume-title":"Proceedings of CADE","author":"W. Bibel","year":"1992","unstructured":"W. Bibel, S. H\u00f6lldobler, and J. W\u00fcrtz. Cycle unification. In D. Kapur, editor, Proceedings of CADE, pages 94\u2013108. Springer, Berlin, 1992."},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"S. Biundo, B. Hummel, D. Hutter, and C. Walther. The Karlsruhe Induction Theorem Proving System. In cade, 1986.","DOI":"10.1007\/3-540-16780-3_132"},{"key":"1_CR18","first-page":"511","volume-title":"Proceedings of IJCAI","author":"K. Bl\u00e4sius","year":"1981","unstructured":"K. Bl\u00e4sius, N. Eisinger, J. Siekmann, G. Smolka, A. Herold, and C. Walther. The Markgraf Karl refutation procedure. In Proceedings of IJCAI, pages 511\u2013518, Los Altos CA, 1981. Morgan Kaufmann."},{"key":"1_CR19","first-page":"57","volume":"2","author":"W. W. Bledsoe","year":"1971","unstructured":"W. W. Bledsoe. Splitting and Reduction Heuristics in Automatic Theorem Proving. AIJ, 2:57\u201378, 1971.","journal-title":"AIJ"},{"key":"1_CR20","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1016\/0304-3975(91)90004-L","volume":"86","author":"R. N. Bol","year":"1991","unstructured":"R. N. Bol, K. R. Apt, and J. W. Klop. An analysis of loop checking mechanisms for logic programming. TCS, 86:35\u201379, 1991.","journal-title":"TCS"},{"key":"1_CR21","volume-title":"PhD thesis","author":"R. Boyer","year":"1971","unstructured":"R. Boyer. Locking: A Restriction of Resolution. PhD thesis, The University of Texas at Austin, 1971."},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"R. S. Boyer and J. S. Moore. A theorem prover for a computational logic. In Mark E. Stickel, editor, Proceedings of CADE, volume 449 of LNAI, pages 1\u201315. Springer Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_75"},{"issue":"4","key":"1_CR23","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"D. Brand. Proving Theorems with the Modification Method. SIAM Journal on Computing, 4(4):412\u2013430, 1975.","journal-title":"SIAM Journal on Computing"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"S. Br\u00fcning. Detecting Non-Provable Goals. In A. Bundy, editor, Proceedings of CADE, volume 814 of LNAI, pages 222\u2013236. Springer Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_16"},{"key":"1_CR25","unstructured":"S. Br\u00fcning. Techniques for Avoiding Redundancy in Theorem Proving Based on the Connection Method. PhD thesis, TH Darmstadt, 1994."},{"key":"1_CR26","first-page":"184","volume":"62","author":"A. Bundy","year":"1993","unstructured":"A. Bundy, A. Stevens, F. van Harmelen, F. Ireland, and A. Smaill. Rippling: A heuristic for guiding inductive proofs. AIJ, 62:184\u2013253, 1993.","journal-title":"AIJ"},{"key":"1_CR27","volume-title":"AIMSA 84, Artificial Intelligence \u2014 Methodology, Systems, Applications, Varna, Bulgaria","author":"E. Eder","year":"1984","unstructured":"E. Eder. An Implementation of a Theorem Prover Based on the Connection Method. In W. Bibel and B. Petkoff, editors, AIMSA 84, Artificial Intelligence \u2014 Methodology, Systems, Applications, Varna, Bulgaria, Amsterdam, September 1984. North-Holland."},{"key":"1_CR28","first-page":"31","volume":"1","author":"E. Eder","year":"1985","unstructured":"E. Eder. Properties of substitutions and unifications. JSC, 1:31\u201346, 1985.","journal-title":"JSC"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"E. Eder. Relative Complexities of First Order Calculi. Vieweg, 1992.","DOI":"10.1007\/978-3-322-84222-0"},{"key":"1_CR30","unstructured":"U. Egly. A Simple Proof for the Pigeonhole Formulae. In B. Neumann, editor, Proceedings of ECAI, pages 70\u201371. John Wiley & Sons, 1992."},{"key":"1_CR31","unstructured":"U. Egly. On Methods of Function Introduction and Related Concepts. PhD thesis, TH Darmstadt, 1994."},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"U. Egly. On the Value of Antiprenexing. In F. Pfenning, editor, Proceedings of LPAR, pages 69\u201383. Springer Verlag, 1994.","DOI":"10.1007\/3-540-58216-9_30"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"C. Ferm\u00fcller, A. Leitsch, T. Tammet, and N. Zamov. Resolution Methods for the Decision Problem. LNCS. Springer-Verlag, 1993. To appear.","DOI":"10.1007\/3-540-56732-1"},{"key":"1_CR34","first-page":"391","volume-title":"Algebra, Combinatorics and Logic in Computer Science","author":"B. Fronh\u00f6fer","year":"1985","unstructured":"B. Fronh\u00f6fer. On refinements of the connection method. In J. Demetrovics, G. Katona, and A. Salomaa, editors, Algebra, Combinatorics and Logic in Computer Science, pages 391\u2013401, Amsterdam, 1985. North-Holland."},{"key":"1_CR35","first-page":"273","volume-title":"Proc. IFIP","author":"H. Gelernter","year":"1959","unstructured":"H. Gelernter. Realization of a geometry theorem-proving machine. In Proc. IFIP, pages 273\u2013282. Paris UNESCO House, 1959."},{"issue":"5","key":"1_CR36","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1016\/0020-0190(93)90210-Z","volume":"45","author":"P. Hanschke","year":"1993","unstructured":"P. Hanschke and J. W\u00fcrtz. Satisfiability of the smallest binary program. Information Processing Letters, 45(5):237\u2013241, April 1993.","journal-title":"Information Processing Letters"},{"key":"1_CR37","unstructured":"R. Letz. First-Order Calculi and Proof Procedures for Automated Deduction. PhD thesis, TH Darmstadt, 1993."},{"issue":"3","key":"1_CR38","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"R. Letz, K. Mayr, and Ch. Goller. Controlled Integrations of the Cut Rule into Connection Tableau Calculi. JAR, 13(3):297\u2013338, 1994. Special Issue on Automated Reasoning with Analytic Tableaux.","journal-title":"JAR"},{"key":"1_CR39","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO \u2014 A High-Performance Theorem Prover for First-Order Logic. JAR, 8:183\u2013212, 1992.","journal-title":"JAR"},{"key":"1_CR40","volume-title":"Automated Theorem Proving: A Logical Basis","author":"D. Loveland","year":"1978","unstructured":"D. Loveland. Automated Theorem Proving: A Logical Basis. North-Holland, New York, 1978."},{"key":"1_CR41","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D. W. Loveland","year":"1986","unstructured":"D. W. Loveland. Mechanical theorem proving by model elimination. JACM, 15:236\u2013251, 1986.","journal-title":"JACM"},{"issue":"3","key":"1_CR42","first-page":"25","volume":"52","author":"J. \u0141ukasiewicz","year":"1948","unstructured":"J. \u0141ukasiewicz. The Shortest Axiom of the Implicational Calculus of Propositions. Proceedings of the Royal Irish Academy, 52(3):25\u201333, April 1948.","journal-title":"Proceedings of the Royal Irish Academy"},{"key":"1_CR43","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0898-1221(76)90002-X","volume":"2","author":"J. McCharen","year":"1976","unstructured":"J. McCharen, R. Overbeek, and L. Wos. Complexity and releted enhancements for automated theorem-proving programs. Computers and Mathematics with Applications, 2:1\u201316, 1976.","journal-title":"Computers and Mathematics with Applications"},{"key":"1_CR44","unstructured":"H. J. Ohlbach. Abstraction Tree Indexing for Terms. In Proceedings of ECAI, 1990."},{"key":"1_CR45","unstructured":"J. Otten and C. Kreitz. A connection based proof method for intuitionistic logic. In this volume."},{"key":"1_CR46","first-page":"47","volume":"16","author":"D. A. Plaisted","year":"1981","unstructured":"D. A. Plaisted. Theorem Proving with Abstraction. AIJ, 16:47\u2013108, 1981.","journal-title":"AIJ"},{"key":"1_CR47","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/BF00244355","volume":"6","author":"D. A. Plaisted","year":"1990","unstructured":"D. A. Plaisted. A Sequent-Style Model Elimination Strategy and a Positive Refinement. JAR, 6:389\u2013402, 1990.","journal-title":"JAR"},{"key":"1_CR48","first-page":"293","volume":"2","author":"D. A. Plaisted","year":"1986","unstructured":"D. A. Plaisted and S. Greenbaum. A Structure-Preserving Clause Form Translation. JSC, 2:293\u2013304, 1986.","journal-title":"JSC"},{"key":"1_CR49","unstructured":"T. Rath. Datenbankunifikation. Diplomarbeit, TH Darmstadt, 1992."},{"issue":"1","key":"1_CR50","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson. A machine-oriented logic based on the resolution principle. JACM, 12(1):23\u201341, 1965.","journal-title":"JACM"},{"key":"1_CR51","doi-asserted-by":"crossref","unstructured":"T. Schaub. A new methodology for query-answering in default logics via structureoriented theorem proving. JAR, 1995. Forthcoming.","DOI":"10.1007\/BF00881832"},{"key":"1_CR52","doi-asserted-by":"crossref","unstructured":"J. Schumann. DELTA \u2014 A bottom-up preprocessor for top-down theorem provers. In A. Bundy, editor, Proceedings of CADE, volume 814 of LNAI, pages 774\u2013777. Springer Verlag, 1994. System description.","DOI":"10.1007\/3-540-58156-1_58"},{"key":"1_CR53","first-page":"51","volume":"7","author":"R. E. Shostak","year":"1976","unstructured":"R. E. Shostak. Refutation Graphs. AIJ, 7:51\u201364, 1976.","journal-title":"AIJ"},{"key":"1_CR54","unstructured":"R. M. Smullyan. First-Order Logic, Ergebnisse der Mathematik und ihrer Grenzgebiete. Springer-Verlag, 1971."},{"key":"1_CR55","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/BF00246025","volume":"2","author":"M. E. Stickel","year":"1986","unstructured":"M. E. Stickel. Schubert's steamroller problem: Formulations and solutions. JAR, 2:89\u2013101, 1986.","journal-title":"JAR"},{"key":"1_CR56","doi-asserted-by":"crossref","unstructured":"M. E. Stickel. A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog. Technical Note 464, SRI International, Artificial Intelligence Center, 1989.","DOI":"10.1007\/3-540-52531-9_135"},{"key":"1_CR57","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe, Ch. Suttner, and T. Yemenis. The TPTP problem library. In A. Bundy, editor, Proceedings of CADE, volume 814 of LNAI, pages 252\u2013266. Springer Verlag, 1994.","DOI":"10.1007\/3-540-58156-1_18"},{"key":"1_CR58","first-page":"234","volume-title":"Studies in Constructive Mathematics and Mathematical Logic, Part II","author":"G. S. Tseitin","year":"1970","unstructured":"G. S. Tseitin. On the Complexity of Derivation in Propositional Calculus. In A. O. Slisenko, editor, Studies in Constructive Mathematics and Mathematical Logic, Part II, pages 234\u2013259. Seminars in Mathematics, V.A. Steklov Mathematical Institute, vol. 8, Leningrad, 1968. English translation: Consultants Bureau, New York, 1970, pp. 115\u2013125."},{"key":"1_CR59","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0167-739X(93)90002-7","volume":"9","author":"R. P. Riet van de","year":"1993","unstructured":"R. P. van de Riet. An overview and appraisal of the fifth generation computer system project. Future Generation Computer Systems Journal, 9:83\u2013103, 1993.","journal-title":"Future Generation Computer Systems Journal"},{"key":"1_CR60","unstructured":"L. A. Wallen. Automated Deduction in Nonclassical Logics. MIT Press, 1990."},{"key":"1_CR61","doi-asserted-by":"crossref","unstructured":"L. Wos, S. Winker, W. McCune, R. Overbeek, E. Lusk, and R. Stevens. Automated reasoning contributes to mathematics and logic. In M. E. Stickel, editor, Proceedings of CADE, pages 485\u2013499. Springer Verlag, 1990.","DOI":"10.1007\/3-540-52885-7_109"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59338-1_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T21:27:08Z","timestamp":1619558828000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59338-1_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540593386","9783540492351"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/3-540-59338-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}