{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:51:24Z","timestamp":1725475884539},"publisher-location":"Berlin, Heidelberg","reference-count":10,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676973"},{"type":"electronic","value":"9783540450085"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722086_23","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T00:43:15Z","timestamp":1167439395000},"page":"279-293","source":"Crossref","is-referenced-by-count":0,"title":["Search Space Compression in Connection Tableau Calculi Using Disjunctive Constraints"],"prefix":"10.1007","author":[{"given":"Ortrun","family":"Ibens","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"23_CR1","volume-title":"Deduction: Automated Logic","author":"W. Bibel","year":"1993","unstructured":"Bibel, W.: Deduction: Automated Logic. Academic Press, London (1993)"},{"key":"23_CR2","first-page":"133","volume-title":"Applied Logic Series 8","author":"W. Bibel","year":"1998","unstructured":"Bibel, W., Br\u00fcning, S., Otten, J., Rath, T., Schaub, T.: Compressions and extensions. In: Applied Logic Series 8, pp. 133\u2013179. Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"23_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M. Fitting","year":"1996","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer, Heidelberg (1996)"},{"key":"23_CR4","unstructured":"Ibens, O.: Connection Tableau Calculi with Disjunctive Constraints. PhD thesis, Institut f\u00fcr Informatik, TU M\u00fcnchen (1999)"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/BFb0027415","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"O. Ibens","year":"1997","unstructured":"Ibens, O., Letz, R.: Subgoal Alternation in Model Elimination. In: Galmiche, D. (ed.) TABLEAUX 1997. LNCS, vol.\u00a01227, pp. 201\u2013215. Springer, Heidelberg (1997)"},{"key":"23_CR6","unstructured":"Letz, R.: First-Order Calculi and Proof Procedures for Automated Deduction. PhD thesis, Technische Hochschule Darmstadt (1993)"},{"key":"23_CR7","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"Letz, R., Mayr, K., Goller, C.: Controlled Integration of the Cut Rule into Connection Tableau Calculi. JAR\u00a013, 297\u2013337 (1994)","journal-title":"JAR"},{"key":"23_CR8","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1023\/A:1005808119103","volume":"18","author":"M. Moser","year":"1997","unstructured":"Moser, M., Ibens, O., Letz, R., Steinbach, J., Goller, C., Schumann, J., Mayr, K.: ETHEO and E-SETHEO - The CADE-13 Systems. JAR\u00a018, 237\u2013246 (1997)","journal-title":"JAR"},{"key":"23_CR9","unstructured":"Ohlbach, H.J.: Abstraction Tree Indexing for Terms. In: Proc. ECAI 1990, pp. 479\u2013484 (1990)"},{"key":"23_CR10","series-title":"LNAI","first-page":"778","volume-title":"Automated Deduction - CADE-12","author":"G. Sutcliffe","year":"1994","unstructured":"Sutcliffe, G., Suttner, C.B., Yemenis, T.: The TPTP problem library. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 778\u2013782. Springer, Heidelberg (1994)"}],"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\/10722086_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,1,25]],"date-time":"2019-01-25T22:32:13Z","timestamp":1548455533000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":10,"URL":"https:\/\/doi.org\/10.1007\/10722086_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}