{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:58:33Z","timestamp":1725494313689},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540662228"},{"type":"electronic","value":"9783540486602"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48660-7_30","type":"book-chapter","created":{"date-parts":[[2007,11,9]],"date-time":"2007-11-09T20:53:07Z","timestamp":1194641587000},"page":"329-343","source":"Crossref","is-referenced-by-count":9,"title":["A Confluent Connection Calculus"],"prefix":"10.1007","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[]},{"given":"Norbert","family":"Eisinger","sequence":"additional","affiliation":[]},{"given":"Ulrich","family":"Furbach","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"unstructured":"F. Baader and K. U. Schulz. Unification Theory. In W. Bibel and P. H. Schmitt, editors, Automated Deduction. A Basis for Applications. Kluwer, 1998.","key":"30_CR1"},{"doi-asserted-by":"crossref","unstructured":"P. Baumgartner. Hyper Tableaux \u2014 The Next Generation. In H. de Swaart, editor, Automated Reasoning with Analytic Tableaux and Related Methods. LNAI 1397, Springer, 1998. 4 This strategy resembles much a tableau procedure-one that takes advantage of confluence, however.","key":"30_CR2","DOI":"10.1007\/3-540-69778-0_14"},{"unstructured":"P. Baumgartner, N. Eisinger, and U. Furbach. A Confluent Connection Calculus. Fachberichte Informatik 23\u201398, Universit\u00e4t Koblenz-Landau, Universit\u00e4t Koblenz-Landau, D-56075 Koblenz, 1998.","key":"30_CR3"},{"doi-asserted-by":"crossref","unstructured":"P. Baumgartner, U. Furbach, and I. Niemel\u00e4. Hyper Tableaux. In Proc. JELIA 96, LNAI 1126. Springer, 1996.","key":"30_CR4","DOI":"10.1007\/3-540-61630-6_1"},{"issue":"3","key":"30_CR5","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BF00881804","volume":"15","author":"B. Beckert","year":"1995","unstructured":"B. Beckert and J. Posegga. leanTAP: Lean tableau-based deduction. Journal of Automated Reasoning, 15(3):339\u2013358, 1995.","journal-title":"Journal of Automated Reasoning"},{"doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg, 2nd edition, 1987.","key":"30_CR6","DOI":"10.1007\/978-3-322-90102-6"},{"doi-asserted-by":"crossref","unstructured":"J.-P. Billon. The Disconnection Method. In P. Miglioli, U. Moscato, D. Mundici, and M. Ornaghi, editors, Theorem Proving with Analytic Tableaux and Related Methods, LNAI 1071. Springer, 1996.","key":"30_CR7","DOI":"10.1007\/3-540-61208-4_8"},{"unstructured":"F. Bry and N. Eisinger. Unit resolution tableaux. Research Report PMS-FB-1996-2, Institut f\u00fcr Informatik, LMU M\u00fcnchen, 1996.","key":"30_CR8"},{"doi-asserted-by":"crossref","unstructured":"M. Fitting. First Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, 1990.","key":"30_CR9","DOI":"10.1007\/978-1-4684-0357-2"},{"unstructured":"H. Fujita and R. Hasegawa. A Model Generation Theorem Prover in KL1 using a Ramified-Stack Algorithm. In Proc.8th of the Eighth International Conference on Logic Programming, pages 535\u2013548, Paris, France, 1991.","key":"30_CR10"},{"unstructured":"R. H\u00e4hnle, B. Beckert, and S. Gerberding. The Many-Valued Theorem Prover 3TAP. Interner Bericht 30\/94, Universit\u00e4t Karlsruhe, 1994.","key":"30_CR11"},{"issue":"6","key":"30_CR12","doi-asserted-by":"publisher","first-page":"819","DOI":"10.1093\/logcom\/6.6.819","volume":"6","author":"R. H\u00e4hnle","year":"1996","unstructured":"R. H\u00e4hnle and S. Klingenbeck. A-Ordered Tableaux. Journal of Logic and Computation, 6(6):819\u2013833, 1996.","journal-title":"Journal of Logic and Computation"},{"doi-asserted-by":"crossref","unstructured":"R. H\u00e4hnle and C. Pape. Ordered tableaux: Extensions and applications. In D. Galmiche, editor, Automated Reasoning with Analytic Tableaux and Related Methods, LNAI 1227, pages 173\u2013187. Springer, 1997.","key":"30_CR13","DOI":"10.1007\/BFb0027413"},{"doi-asserted-by":"crossref","unstructured":"S. Klingenbeck and R. H\u00e4hnle. Semantic tableaux with ordering restrictions. In A. Bundy, editor, CADE 12, LNAI 814, pages 708\u2013722. Springer, 1994.","key":"30_CR14","DOI":"10.1007\/3-540-58156-1_51"},{"doi-asserted-by":"crossref","unstructured":"D. Loveland. Mechanical Theorem Proving by Model Elimination. JACM, 15(2), 1968.","key":"30_CR15","DOI":"10.1145\/321450.321456"},{"key":"30_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/BFb0012847","volume-title":"CADE 9","author":"R. Manthey","year":"1988","unstructured":"R. Manthey and F. Bry. SATCHMO: a theorem prover implemented in Prolog. In E. Lusk and R. Overbeek, editors, CADE 9, LNCS 310, pages 415\u2013434. Springer, 1988."},{"unstructured":"D. A. Plaisted and Y. Zhu. Ordered Semantic Hyper Linking. In Proceedings of AAAI-97, 1997.","key":"30_CR17"},{"key":"30_CR18","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","volume":"26","author":"D. Prawitz","year":"1960","unstructured":"D. Prawitz. An improved proof procedure. Theoria, 26:102\u2013139, 1960.","journal-title":"Theoria"},{"unstructured":"A. Voronkov. Strategies in rigid-variable methods. In IJCAI 97, Nagoya, 1997.","key":"30_CR19"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-16"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48660-7_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,4]],"date-time":"2019-05-04T08:56:35Z","timestamp":1556960195000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48660-7_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540662228","9783540486602"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-48660-7_30","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}