{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T11:03:11Z","timestamp":1775818991966,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642221187","type":"print"},{"value":"9783642221194","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-22119-4_18","type":"book-chapter","created":{"date-parts":[[2011,6,15]],"date-time":"2011-06-15T10:21:08Z","timestamp":1308133268000},"page":"226-241","source":"Crossref","is-referenced-by-count":13,"title":["A Non-clausal Connection Calculus"],"prefix":"10.1007","author":[{"given":"Jens","family":"Otten","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"18_CR1","doi-asserted-by":"publisher","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. Journal of the ACM\u00a028, 193\u2013214 (1981)","journal-title":"Journal of the ACM"},{"key":"18_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-006-9055-9","volume":"38","author":"R. Antonsen","year":"2007","unstructured":"Antonsen, R., Waaler, A.: Liberalized Variable Splitting. Journal of Automated Reasoning\u00a038, 3\u201330 (2007)","journal-title":"Journal of Automated Reasoning"},{"key":"18_CR3","doi-asserted-by":"publisher","first-page":"844","DOI":"10.1145\/182.183","volume":"26","author":"W. Bibel","year":"1983","unstructured":"Bibel, W.: Matings in Matrices. Communications of the ACM\u00a026, 844\u2013852 (1983)","journal-title":"Communications of the ACM"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Automated Theorem Proving. Vieweg, Wiesbaden (1987)","DOI":"10.1007\/978-3-322-90102-6"},{"key":"18_CR5","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BF01201353","volume":"39","author":"G. Gentzen","year":"1935","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Mathematische Zeitschrift\u00a039, 176\u2013210, 405\u2013431 (1935)","journal-title":"Mathematische Zeitschrift"},{"key":"18_CR6","first-page":"100","volume-title":"Handbook of Automated Reasoning","author":"R. H\u00e4hnle","year":"2001","unstructured":"H\u00e4hnle, R.: Tableaux and Related Methods. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 100\u2013178. Elsevier, Amsterdam (2001)"},{"key":"18_CR7","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1016\/j.tcs.2004.09.001","volume":"328","author":"R. H\u00e4hnle","year":"2004","unstructured":"H\u00e4hnle, R., Murray, N.V., Rosenthal, E.: Linearity and Regularity with Negation Normal Form. Theoretical Computer Science\u00a0328, 325\u2013354 (2004)","journal-title":"Theoretical Computer Science"},{"key":"18_CR8","first-page":"88","volume":"5","author":"C. Kreitz","year":"1999","unstructured":"Kreitz, C., Otten, J.: Connection-based Theorem Proving in Classical and Non-classical Logics. Journal of Universal Computer Science\u00a05, 88\u2013112 (1999)","journal-title":"Journal of Universal Computer Science"},{"key":"18_CR9","doi-asserted-by":"publisher","first-page":"2015","DOI":"10.1016\/B978-044450813-3\/50030-8","volume-title":"Handbook of Automated Reasoning","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Model Elimination and Connection Tableau Procedures. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 2015\u20132114. Elsevier, Amsterdam (2001)"},{"key":"18_CR10","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1145\/321450.321456","volume":"15","author":"D. Loveland","year":"1968","unstructured":"Loveland, D.: Mechanical Theorem-Proving by Model Elimination. Journal of the ACM\u00a015, 236\u2013251 (1968)","journal-title":"Journal of the ACM"},{"key":"18_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/11554554_19","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J. Otten","year":"2005","unstructured":"Otten, J.: Clausal Connection-Based Theorem Proving in Intuitionistic First-Order Logic. In: Beckert, B. (ed.) TABLEAUX 2005. LNCS (LNAI), vol.\u00a03702, pp. 245\u2013261. Springer, Heidelberg (2005)"},{"key":"18_CR12","doi-asserted-by":"crossref","first-page":"159","DOI":"10.3233\/AIC-2010-0464","volume":"23","author":"J. Otten","year":"2010","unstructured":"Otten, J.: Restricting Backtracking in Connection Calculi. AI Communications\u00a023, 159\u2013182 (2010)","journal-title":"AI Communications"},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1016\/S0747-7171(03)00037-3","volume":"36","author":"J. Otten","year":"2003","unstructured":"Otten, J., Bibel, W.: leanCoP: Lean Connection-based Theorem Proving. Journal of Symbolic Computation\u00a036, 139\u2013161 (2003)","journal-title":"Journal of Symbolic Computation"},{"key":"18_CR14","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. Plaisted","year":"1986","unstructured":"Plaisted, D., Greenbaum, S.: A Structure-preserving Clause Form Translation. Journal of Symbolic Computation\u00a02, 293\u2013304 (1986)","journal-title":"Journal of Symbolic Computation"},{"key":"18_CR15","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"A. Robinson","year":"1965","unstructured":"Robinson, A.: A Machine-oriented Logic Based on the Resolution Principle. Journal of the ACM\u00a012, 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"key":"18_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/3-540-45744-5_34","volume-title":"Automated Reasoning","author":"S. Schmitt","year":"2001","unstructured":"Schmitt, S., Lorigo, L., Kreitz, C., Nogin, A.: JProver: Integrating Connection-Based Theorem Proving into Interactive Proof Assistants. In: Gor\u00e9, R., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 421\u2013426. Springer, Heidelberg (2001)"},{"key":"18_CR17","doi-asserted-by":"publisher","first-page":"1487","DOI":"10.1016\/B978-044450813-3\/50024-2","volume-title":"Handbook of Automated Reasoning","author":"A. Waaler","year":"2001","unstructured":"Waaler, A.: Connections in Nonclassical Logics. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, pp. 1487\u20131578. Elsevier, Amsterdam (2001)"},{"key":"18_CR18","volume-title":"Automated Deduction in Nonclassical Logics","author":"L. Wallen","year":"1990","unstructured":"Wallen, L.: Automated Deduction in Nonclassical Logics. MIT Press, Washington (1990)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22119-4_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,20]],"date-time":"2020-06-20T00:55:52Z","timestamp":1592614552000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22119-4_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642221187","9783642221194"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22119-4_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}