{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:01:07Z","timestamp":1725490867217},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540735946"},{"type":"electronic","value":"9783540735953"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73595-3_36","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"492-507","source":"Crossref","is-referenced-by-count":15,"title":["Hyper Tableaux with Equality"],"prefix":"10.1007","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[]},{"given":"Ulrich","family":"Furbach","sequence":"additional","affiliation":[]},{"given":"Bj\u00f6rn","family":"Pelzer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"36_CR1","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1093\/logcom\/7.1.39","volume":"7","author":"B. Beckert","year":"1997","unstructured":"Beckert, B.: Semantic Tableaux With Equality. Journal of Logic and Computation\u00a07(1), 39\u201358 (1997)","journal-title":"Journal of Logic and Computation"},{"key":"36_CR2","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Furbach, U.: Automated Deduction Techniques for the Management of Personalized Documents. Annals of Mathematics and Artificial Intelligence 38(1) (2003)","DOI":"10.1023\/A:1022976016809"},{"key":"36_CR3","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Furbach, U., Gross-Hardt, M., Sinner, A.: Living Book \u2013 Deduction, Slicing, and Interaction. J. of Aut. Reasoning 32(3) (2004)","DOI":"10.1023\/B:JARS.0000044872.51237.c9"},{"key":"36_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Logics in Artificial Intelligence","author":"P. Baumgartner","year":"1996","unstructured":"Baumgartner, P., Furbach, U., Niemel\u00e4, I.: Hyper Tableaux. In: Or\u0142owska, E., Alferes, J.J., Moniz Pereira, L. (eds.) JELIA 1996. LNCS, vol.\u00a01126, Springer, Heidelberg (1996)"},{"key":"36_CR5","volume-title":"Automated Deduction. A Basis for Applications","author":"L. Bachmair","year":"1998","unstructured":"Bachmair, L., Ganzinger, H.: Chapter 11: Equational Reasoning in Saturation-Based Theorem Proving. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction. A Basis for Applications, vol.\u00a01, Kluwer, Dordrecht (1998)"},{"key":"36_CR6","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_11","volume-title":"Automated Reasoning","author":"P. Baumgartner","year":"2006","unstructured":"Baumgartner, P., Schmidt, R.: Blocking and Other Enhancements for Bottom-up Model Generation Methods. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, Springer, Heidelberg (2006)"},{"key":"36_CR7","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-20","author":"P. Baumgartner","year":"2005","unstructured":"Baumgartner, P., Tinelli, C.: The Model Evolution Calculus with Equality. In: Nieuwenhuis, R. (ed.) Automated Deduction \u2013 CADE-20. LNCS (LNAI), vol.\u00a03632, Springer, Heidelberg (2005)"},{"key":"36_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Design and Implementation of Symbolic Computation Systems","author":"A. Degtyarev","year":"1996","unstructured":"Degtyarev, A., Voronkov, A.: Equality Elimination for the Tableau Method. In: Limongelli, C., Calmet, J. (eds.) DISCO 1996. LNCS, vol.\u00a01128, Springer, Heidelberg (1996)"},{"issue":"1","key":"36_CR9","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1023\/A:1005996623714","volume":"20","author":"A. Degtyarev","year":"1998","unstructured":"Degtyarev, A., Voronkov, A.: What you Always Wanted to Know About Rigid E-Unification. Journal of Automated Reasoning\u00a020(1), 47\u201380 (1998)","journal-title":"Journal of Automated Reasoning"},{"key":"36_CR10","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69912-5_14","volume-title":"KI 2006: Advances in Artificial Intelligence","author":"U. Furbach","year":"2007","unstructured":"Furbach, U., Obermaier, C.: Applications of Automated Reasoning. In: Freksa, C., Kohlhase, M., Schill, K. (eds.) KI 2006. LNCS (LNAI), vol.\u00a04314, Springer, Heidelberg (2007)"},{"key":"36_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45744-5_46","volume-title":"Automated Reasoning","author":"M. Giese","year":"2001","unstructured":"Giese, M.: Incremental Closure of Free Variable Tableaux. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, Springer, Heidelberg (2001)"},{"key":"36_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45616-3_10","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M. Giese","year":"2002","unstructured":"Giese, M.: A Model Generation Style Completeness Proof For Constraint Tableaux With Superposition. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, Springer, Heidelberg (2002)"},{"key":"36_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"M. Giese","year":"2003","unstructured":"Giese, M.: Simplification Rules for Constrained Formula Tableaux. In: Mayer, M.C., Pirri, F. (eds.) TABLEAUX 2003. LNCS, vol.\u00a02796, Springer, Heidelberg (2003)"},{"key":"36_CR14","doi-asserted-by":"crossref","unstructured":"Letz, R., Mayr, K., Goller, C.: Controlled Integrations of the Cut Rule into Connection Tableau Calculi. J. of Aut. Reasoning 13 (1994)","DOI":"10.1007\/BF00881947"},{"key":"36_CR15","series-title":"Lecture Notes in Artificial Intelligence","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, Springer, Heidelberg (2002)"},{"key":"36_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0012847","volume-title":"9th International Conference on Automated Deduction","author":"R. Manthey","year":"1988","unstructured":"Manthey, R., Bry, F.: SATCHMO: a Theorem Prover Implemented in Prolog. In: Lusk, E.R., Overbeek, R. (eds.) 9th International Conference on Automated Deduction. LNCS, vol.\u00a0310, Springer, Heidelberg (1988)"},{"issue":"2","key":"36_CR17","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/BF00245458","volume":"9","author":"W. McCune","year":"1992","unstructured":"McCune, W.: Experiments with Discrimination-Tree Indexing and Path Indexing for Term Retrieval. J. of Aut. Reasoning\u00a09(2), 147\u2013167 (1992)","journal-title":"J. of Aut. Reasoning"},{"key":"36_CR18","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based Theorem Proving. In: Robinson, J.A., Voronkov, A. (eds.) Handbook of Automated Reasoning, Elsevier and MIT Press (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"key":"36_CR19","series-title":"Lecture Notes in Computer Science","volume-title":"CADE-21","author":"B. Pelzer","year":"2007","unstructured":"Pelzer, B., Wernhard, C.: System Description: E-KRHyper. In: Pfenning, F. (ed.) CADE-21. LNCS, Springer, Heidelberg (2007)"},{"issue":"1","key":"36_CR20","first-page":"35","volume":"19","author":"G. Sutcliffe","year":"2006","unstructured":"Sutcliffe, G., Suttner, C.: The State of CASC. AI Communications\u00a019(1), 35\u201348 (2006)","journal-title":"AI Communications"},{"key":"36_CR21","doi-asserted-by":"crossref","unstructured":"Weidenbach, C.: Combining Superposition, Sorts and Splitting. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning. North Holland (2001)","DOI":"10.1016\/B978-044450813-3\/50029-1"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_36.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T09:53:10Z","timestamp":1619517190000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540735946","9783540735953"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}