{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T01:22:48Z","timestamp":1755220968128,"version":"3.43.0"},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2002,3,1]],"date-time":"2002-03-01T00:00:00Z","timestamp":1014940800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,3,1]],"date-time":"2002-03-01T00:00:00Z","timestamp":1014940800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Studia Logica"],"published-print":{"date-parts":[[2002,3]]},"DOI":"10.1023\/a:1015134701251","type":"journal-article","created":{"date-parts":[[2002,12,28]],"date-time":"2002-12-28T17:32:56Z","timestamp":1041096776000},"page":"241-270","source":"Crossref","is-referenced-by-count":1,"title":["Connection Tableau Calculi with Disjunctive Constraints"],"prefix":"10.1007","volume":"70","author":[{"given":"Ortrun","family":"Ibens","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"407884_CR1","first-page":"52","volume":"5","author":"T. Baar","year":"1999","unstructured":"Baar, T., B. Fischer, and D. Fuchs, 'Integrating deduction techniques in a software reuse application', Journal of Universal Computer Science 5(3):52-72, 1999.","journal-title":"Journal of Universal Computer Science"},{"key":"407884_CR2","volume-title":"Deduction: Automated Logic","author":"W. Bibel","year":"1993","unstructured":"Bibel, W., Deduction: Automated Logic, Academic Press, London, 1993."},{"key":"407884_CR3","doi-asserted-by":"crossref","unstructured":"Bibel, W., S. Br\u00dcning, J. Otten, T. Rath, and T. Schaub, 'Compressions and extensions', in W. Bibel and P. H. Schmitt (eds.), Automated Deduction \u2014 A Basis for Applications, volume 8 of Applied Logic Series, chapter 5, pages 133-179, Kluwer Academic Publishers, 1998.","DOI":"10.1007\/978-94-017-0435-9"},{"issue":"4","key":"407884_CR4","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1137\/0204036","volume":"4","author":"D. Brand","year":"1975","unstructured":"Brand, D., 'Proving theorems with the modification method', SIAM Journal of Computing 4(4):412-430, 1975.","journal-title":"SIAM Journal of Computing"},{"key":"407884_CR5","doi-asserted-by":"crossref","unstructured":"Fischer, B., J. Schumann, and G. Snelting, 'Deduction-based software component retrieval', in W. Bibel and P. H. Schmitt (eds.), Automated Deduction \u2014 A Basis for Applications, volume 10 of Applied Logic Series, chapter 11, pages 265-292, Kluwer Academic Publishers, 1998.","DOI":"10.1007\/978-94-017-0437-3_11"},{"key":"407884_CR6","doi-asserted-by":"crossref","unstructured":"Fitting, M., First-Order Logic and Automated Theorem Proving, Springer, 1996.","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"407884_CR7","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1016\/0304-3975(89)90004-2","volume":"67","author":"J. Gallier","year":"1989","unstructured":"Gallier, J., and W. Snyder, 'Complete sets of transformations for general e-unification', Theoretical Computer Science 67:203-260, 1989.","journal-title":"Theoretical Computer Science"},{"key":"407884_CR8","doi-asserted-by":"crossref","unstructured":"Graf, P., and D. Fehrer, 'Term indexing', in W. Bibel and P. H. Schmitt (eds.), Automated Deduction \u2014 A Basis for Applications, volume 9 of Applied Logic Series, chapter 5, pages 125-147, Kluwer Academic Publishers, 1998.","DOI":"10.1007\/978-94-017-0435-9_5"},{"key":"407884_CR9","doi-asserted-by":"crossref","unstructured":"Ibens, O., 'Automated theorem proving with disjunctive constraints', in J. Jaffar (ed.), Principles and Practice of Constraint Programming \u2014 CP'99, volume 1713 of Lecture Notes in Computer Science, pages 484-485, Springer, October 1999.","DOI":"10.1007\/978-3-540-48085-3_38"},{"key":"407884_CR10","volume-title":"Connection Tableau Calculi with Disjunctive Constraints","author":"O. Ibens","year":"1999","unstructured":"Ibens, O., Connection Tableau Calculi with Disjunctive Constraints, PhD thesis, Institut f\u00fcr Informatik, TU M\u00fcnchen, 1999."},{"key":"407884_CR11","doi-asserted-by":"crossref","unstructured":"Ibens, O., 'Search space compression in connection tableau calculi using disjunctive constraints', in Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2000), Lecture Notes in Artificial Intelligence, Springer, 2000.","DOI":"10.1007\/10722086_23"},{"key":"407884_CR12","doi-asserted-by":"crossref","unstructured":"Ibens, O., and R. Letz, 'Subgoal alternation in model elimination', in TABLEAUX'97, volume 1227 of Lecture Notes in Artificial Intelligence, pages 201-215, Springer, 1997.","DOI":"10.1007\/BFb0027415"},{"key":"407884_CR13","unstructured":"Letz, R., First-Order Calculi and Proof Procedures for Automated Deduction, PhD thesis, Technische Hochschule Darmstadt, 1993."},{"key":"407884_CR14","doi-asserted-by":"crossref","first-page":"297","DOI":"10.1007\/BF00881947","volume":"13","author":"R. Letz","year":"1994","unstructured":"Letz, R., K. Mayr, and C. Goller, 'Controlled integration of the cut rule into connection tableau calculi', Journal of Automated Reasoning 13:297-337, 1994.","journal-title":"Journal of Automated Reasoning"},{"issue":"19","key":"407884_CR15","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1023\/A:1005843212881","volume":"3","author":"W. W. McCune","year":"1997","unstructured":"McCune, W. W., 'Solution of the Robbins problem', Journal of Automated Reasoning 3(19):263-276, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"407884_CR16","doi-asserted-by":"crossref","first-page":"237","DOI":"10.1023\/A:1005808119103","volume":"18","author":"M. Moser","year":"1997","unstructured":"Moser, M., O. Ibens, R. Letz, J. Steinbach, C. Goller, J. Schumann, and K. Mayr, 'SETHEO and E-SETHEO \u2014 The CADE-13 systems', Journal of Automated Reasoning 18:237-246, 1997.","journal-title":"Journal of Automated Reasoning"},{"key":"407884_CR17","unstructured":"Moser, M., and J. Steinbach, 'STE-Modification revisited', Technical Report AR-97-03, Technische Universit\u00e4t M\u00fcnchen, Institut f\u00fcr Informatik, 1997."},{"key":"407884_CR18","unstructured":"Ohlbach, H. J., 'Abstraction tree indexing for terms', in ECAI-90, Proceedings of the 9th European Conference on Artificial Intelligence, pages 479-484, Stockholm, 1990."},{"key":"407884_CR19","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00297245","volume":"4","author":"M. E. Stickel","year":"1988","unstructured":"Stickel, M. E., 'A Prolog technology theorem prover: Implementation by an extended Prolog compiler', Journal of Automated Reasoning 4:353-380, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"407884_CR20","doi-asserted-by":"crossref","unstructured":"Sutcliffe, G., C. B. Suttner, and T. Yemenis, 'The TPTP problem library', in A. Bundy (ed.), Automated Deduction \u2014 CADE-12, volume 814 of Lecture Notes in Artificial Intelligence, pages 778-782, Springer, 1994.","DOI":"10.1007\/3-540-58156-1_18"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1015134701251.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1015134701251\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1015134701251.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:21:31Z","timestamp":1754630491000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1015134701251"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,3]]},"references-count":20,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,3]]}},"alternative-id":["407884"],"URL":"https:\/\/doi.org\/10.1023\/a:1015134701251","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2002,3]]}}}