{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:05:50Z","timestamp":1725573950609},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540407874"},{"type":"electronic","value":"9783540452065"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-45206-5_11","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T00:17:05Z","timestamp":1294359425000},"page":"117-133","source":"Crossref","is-referenced-by-count":4,"title":["Universal Variables in Disconnection Tableaux"],"prefix":"10.1007","author":[{"given":"Reinhold","family":"Letz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gernot","family":"Stenz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Foundations: Calculi and Methods","first-page":"353","volume-title":"Automated Deduction: A Basis for Applications","author":"L. Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H.: Equational reasoning in saturation-based theorem proving. In: Automated Deduction: A Basis for Applications. Foundations: Calculi and Methods, vol.\u00a0I, pp. 353\u2013398. Kluwer, Dordrecht (1998)"},{"key":"11_CR2","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/3-540-69778-0_14","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"P. Baumgartner","year":"1998","unstructured":"Baumgartner, P.: Hyper tableau \u2013 the next generation. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, pp. 60\u201376. Springer, Heidelberg (1998)"},{"key":"11_CR3","series-title":"Foundations","first-page":"11","volume-title":"Automated Deduction \u2014 A Basis for Applications","author":"B. Beckert","year":"1998","unstructured":"Beckert, B., H\u00e4hnle, R.: Analytic tableaux. In: Automated Deduction \u2014 A Basis for Applications. Foundations, vol.\u00a0I, pp. 11\u201341. Kluwer, Dordrecht (1998)"},{"unstructured":"Bibel, W., Letz, R., Schumann, J.: Bottom-up enhancements of deductive systems. Artifial Intelligence and Information-Control Systems of Robots, 1\u20139 (1987)","key":"11_CR4"},{"key":"11_CR5","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/3-540-61208-4_8","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"J.-P. Billon","year":"1996","unstructured":"Billon, J.-P.: The disconnection method: a confluent integration of unification in the analytic framework. In: Miglioli, P., Moscato, U., Ornaghi, M., Mundici, D. (eds.) TABLEAUX 1996. LNCS (LNAI), vol.\u00a01071, pp. 110\u2013126. Springer, Heidelberg (1996)"},{"key":"11_CR6","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"M.C. Fitting","year":"1996","unstructured":"Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer, Heidelberg (1996)","edition":"2"},{"key":"11_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-69778-0_9","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"U. Hustadt","year":"1998","unstructured":"Hustadt, U., Schmidt, R., Weidenbach, C.: Optimised functional translation and resolution. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, pp. 36\u201337. Springer, Heidelberg (1998)"},{"doi-asserted-by":"crossref","unstructured":"Lee, S.-J., Plaisted, D.: Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning, 25\u201342 (1992)","key":"11_CR8","DOI":"10.1007\/BF00247825"},{"issue":"2","key":"11_CR9","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1023\/A:1005839531398","volume":"18","author":"R. Letz","year":"1997","unstructured":"Letz, R.: LINUS: A link instantiation prover with unit support. Journal of Automated Reasoning\u00a018(2), 205\u2013210 (1997)","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR10","series-title":"Foundations","first-page":"43","volume-title":"Automated Deduction \u2014 A Basis for Applications","author":"R. Letz","year":"1998","unstructured":"Letz, R.: Clausal tableaux. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction \u2014 A Basis for Applications. Foundations, vol.\u00a0I, pp. 43\u201372. Kluwer, Dordrecht (1998)"},{"key":"11_CR11","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-45616-3_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R.: Lemma and model caching in decision procedures for quantified boolean formulas. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS, vol.\u00a02381, pp. 160\u2013175. Springer, Heidelberg (2002)"},{"issue":"3","key":"11_CR12","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. Journal of Automated Reasoning\u00a013(3), 297\u2013337 (1994)","journal-title":"Journal of Automated Reasoning"},{"issue":"2","key":"11_CR13","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S., Bibel, W.: SETHEO: A high-performance theorem prover. Journal of Automated Reasoning\u00a08(2), 183\u2013212 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"11_CR14","first-page":"142","volume-title":"Proceedings, 8th LPAR, Havanna, Cuba","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Proof and Model Generation with Disconnection Tableaux. In: Voronkov, A. (ed.) Proceedings, 8th LPAR, Havanna, Cuba, pp. 142\u2013156. Springer, Berlin (2001)"},{"key":"11_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/3-540-45616-3_13","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R., Stenz, G.: Integration of Equality Reasoning into the Disconnection Calculus. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 176\u2013190. Springer, Heidelberg (2002)"},{"key":"11_CR16","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/3-540-45744-5_29","volume-title":"Automated Reasoning","author":"A. Riazanov","year":"2001","unstructured":"Riazanov, A., Voronkov, A.: Vampire 1.1 (System description). In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 376\u2013380. Springer, Heidelberg (2001)"},{"key":"11_CR17","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0004-3702(76)90021-7","volume":"7","author":"R.E. Shostak","year":"1976","unstructured":"Shostak, R.E.: Refutation graphs. Artificial Intelligence\u00a07, 51\u201364 (1976)","journal-title":"Artificial Intelligence"},{"key":"11_CR18","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/3-540-45616-3_24","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"G. Stenz","year":"2002","unstructured":"Stenz, G.: DCTP 1.2 - system abstract. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 335\u2013340. Springer, Heidelberg (2002)"},{"unstructured":"Stenz, G.: The Disconnection Calculus. Dissertation, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t Munchen. Logos Verlag, Berlin (2002)","key":"11_CR19"},{"key":"11_CR20","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/10722086_34","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"G. Stenz","year":"2000","unstructured":"Stenz, G., Wolf, A.: E-SETHEO: An Automated3 Theorem Prover - System Abstract. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS (LNAI), vol.\u00a01847, pp. 436\u2013440. Springer, Heidelberg (2000)"},{"unstructured":"Sutcliffe, G., Suttner, C.: The CADE-14 ATP system competition. Technical Report JCU-CS-98\/01, Department of Computer Science, James Cook University, March 3 (1998)","key":"11_CR21"},{"key":"11_CR22","series-title":"Lecture Notes in Computer Science","first-page":"708","volume-title":"Automated Deduction - CADE-12","author":"G. Sutcliffe","year":"1994","unstructured":"Sutcliffe, G., Suttner, C., Yemenis, T.: The TPTP problem library. In: Bundy, A. (ed.) CADE 1994. LNCS, vol.\u00a0814, pp. 708\u2013722. Springer, Heidelberg (1994)"},{"issue":"2","key":"11_CR23","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1023\/A:1005812220011","volume":"18","author":"C. Weidenbach","year":"1997","unstructured":"Weidenbach, C.: Spass - version 0.49. Journal of Automated Reasoning\u00a018(2), 247\u2013252 (1997)","journal-title":"49. Journal of Automated Reasoning"},{"key":"11_CR24","volume-title":"Handbook of Automated Reasoning","author":"C. Weidenbach","year":"1999","unstructured":"Weidenbach, C.: Combining Superposition, Sorts and Splitting. In: Handbook of Automated Reasoning. Elsevier, Amsterdam (1999)"}],"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-540-45206-5_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T06:37:39Z","timestamp":1553323059000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45206-5_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540407874","9783540452065"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45206-5_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}