{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:29:13Z","timestamp":1725542953984},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540370338"},{"type":"electronic","value":"9783540370352"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11811220_12","type":"book-chapter","created":{"date-parts":[[2006,7,24]],"date-time":"2006-07-24T12:40:48Z","timestamp":1153744848000},"page":"127-138","source":"Crossref","is-referenced-by-count":0,"title":["Hyper Tableaux \u2014 The Third Version"],"prefix":"10.1007","author":[{"given":"Shasha","family":"Feng","sequence":"first","affiliation":[]},{"given":"Jigui","family":"Sun","sequence":"additional","affiliation":[]},{"given":"Xia","family":"Wu","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Baumgartner, P., Furbach, U., Niemel\u00e4, I.: Hyper Tableaux (long version) (December 1996), from: http:\/\/www.uni-koblenz.de\/fb4","DOI":"10.1007\/3-540-61630-6_1"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","first-page":"1","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, pp. 1\u201317. Springer, Heidelberg (1996)"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","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 Tableaux\u2014The Next Generation. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS, vol.\u00a01397, pp. 60\u201376. Springer, Heidelberg (1998)"},{"key":"12_CR4","volume-title":"Symbolic Logic and Mechanical Theorem Proving","author":"C. Chang","year":"1973","unstructured":"Chang, C., Lee, R.: Symbolic Logic and Mechanical Theorem Proving. Academic Press, London (1973)"},{"key":"12_CR5","series-title":"Texts and monographs in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-0357-2","volume-title":"First Order Logic and Automated Theorem Proving","author":"M. Fitting","year":"1990","unstructured":"Fitting, M.: First Order Logic and Automated Theorem Proving. Texts and monographs in Computer Science. Springer, Heidelberg (1990)"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Letz, R., Mayr, K., Goller, C.: Controlled integrations of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning\u00a013 (1994)","DOI":"10.1007\/BF00881947"},{"key":"12_CR7","series-title":"LNAI","volume-title":"Automated Deduction - CADE-17","author":"P. Baumgartner","year":"2000","unstructured":"Baumgartner, P.: FDPLL\u2014A First-Order Davis-Putnam-Logeman-Loveland Procedure. In: McAllester, D. (ed.) CADE 2000. LNCS (LNAI), vol.\u00a01831. Springer, Heidelberg (2000)"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/978-3-540-45085-6_32","volume-title":"Automated Deduction \u2013 CADE-19","author":"P. Baumgartner","year":"2003","unstructured":"Baumgartner, P., Tinelli, C.: The Model Evolution Calculus. In: Baader, F. (ed.) CADE 2003. LNCS, vol.\u00a02741, pp. 350\u2013364. Springer, Heidelberg (2003)"},{"key":"12_CR9","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-45653-8_10","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Letz","year":"2001","unstructured":"Letz, R., Stenz, G.: Proof and Model Generation with Disconnection Tableaux. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 142\u2013156. Springer, Heidelberg (2001)"},{"key":"12_CR10","unstructured":"Letz, R.: First-Order Calculi and Proof Procedures for Automated Deduction. Darmstadt: Technische Hochschule Darmstadt (1993)"},{"key":"12_CR11","series-title":"LNAI","volume-title":"KI-97: Advances in Artificial Intelligence","author":"M. Kuhn","year":"1997","unstructured":"Kuhn, M.: Rigid Hypertableaux. In: Brewka, G., Habel, C., Nebel, B. (eds.) KI 1997. LNCS (LNAI), vol.\u00a01303. Springer, Heidelberg (1997)"},{"key":"12_CR12","first-page":"227","volume":"1","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: Automated deduction with hyper-resolution. I. J. Comput. Math.\u00a01, 227\u2013234 (1965)","journal-title":"I. J. Comput. Math."},{"key":"12_CR13","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/0004-3702(76)90010-2","volume":"7","author":"D. Brand","year":"1976","unstructured":"Brand, D.: Analytic Resolution in Theorem Proving. Artificial Intelligence\u00a07, 285\u2013318 (1976)","journal-title":"Artificial Intelligence"}],"container-title":["Lecture Notes in Computer Science","Knowledge Science, Engineering and Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11811220_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:13:48Z","timestamp":1605644028000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11811220_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540370338","9783540370352"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/11811220_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}