{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,29]],"date-time":"2026-09-29T12:59:04Z","timestamp":1790686744908,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540616306","type":"print"},{"value":"9783540706434","type":"electronic"}],"license":[{"start":{"date-parts":[[1996,1,1]],"date-time":"1996-01-01T00:00:00Z","timestamp":820454400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61630-6_1","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T22:08:22Z","timestamp":1330294102000},"page":"1-17","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":64,"title":["Hyper tableaux"],"prefix":"10.1007","author":[{"given":"Peter","family":"Baumgartner","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ulrich","family":"Furbach","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ilkka","family":"Niemel\u00e4","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"1_CR1","volume-title":"Hyper Tableaux and Disjunctive Logic Programming","author":"P. Baumgartner","year":"1996","unstructured":"Peter Baumgartner and Ulrich Furbach. Hyper Tableaux and Disjunctive Logic Programming. Fachberichte Informatik 13-96, Universit\u00e4t Koblenz-Landau, Universit\u00e4t Koblenz-Landau, Institut f\u00fcr Informatik, Rheinau 1, D-56075 Koblenz, 1996."},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"B. Beckert and R. H\u00e4hnle. An Improved Method for Adding Equality to Free Variable semantic Tableaux. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume 607 of LNCS, pages 507\u2013521. Springer, 1992.","DOI":"10.1007\/3-540-55602-8_188"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Bernhard Beckert and Joachim Posegga. leanTAP: Lean tableaubased deduction. Journal of Automated Reasoning, 1994. To appear.","DOI":"10.1007\/3-540-58156-1_62"},{"key":"1_CR4","unstructured":"Jean-Paul Billon. The Disconnection Method. In P. Moscato, U. Moscato, D. Mundici, and M. Ornaghi, editors, Theorem Proving with Analytic Tableaux and Related Methods, volume 1071 of Lecture Notes in Artificial Intelligence. Springer, 1996."},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"F. Bry and A. Yaha. Minimal model generation with unit hyper-resolution tableau. In 5th Workshop of Analytic Tableaux and Related methods, LNCS. Springer, 1996.","DOI":"10.1007\/3-540-61208-4_10"},{"key":"1_CR6","unstructured":"C. Chang and R. Lee. Symbolic Logic and Mechanical Theorem Proving. Academic Press, 1973."},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"M. Fitting. First Order Logic and Automated Theorem Proving. Texts and Monographs in Computer Science. Springer, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"1_CR8","unstructured":"H. Fujita and R. Hasegawa. A Model Generation Theorem Prover in KL1 using a Ramified-Stack Algorithm. In Proc. of the Eigth International Conference on Logic Programming, pages 535\u2013548, Paris, France, 1991."},{"key":"1_CR9","unstructured":"R. H\u00e4hnle, B. Beckert, and S. Gerberding. The Many-Valued Theorem Prover 3TAP. Interner Bericht 30\/94, Universit\u00e4t Karlsruhe, 1994."},{"key":"1_CR10","unstructured":"R. H\u00e4hnle. Positive tableaux. Research note, 1995."},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"R. Letz, K. Mayr, and C. Goller. Controlled Integrations of the Cut Rule into Connection Tableau Calculi. Journal of Automated Reasoning, 13, 1994.","DOI":"10.1007\/BF00881947"},{"key":"1_CR12","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/BF00881861","volume":"14","author":"D. Loveland","year":"1995","unstructured":"D. Loveland, D. Reed, and D. Wilson. SATCHMORE: SATCHMO with RElevance. Journal of Autmated Reasoning, 14:325\u2013351, 1995.","journal-title":"Journal of Autmated Reasoning"},{"key":"1_CR13","unstructured":"R. Manthey and F. Bry. SATCHMO: a theorem prover implemented in Prolog. In Proc. 9th CADE. Argonnee, Illinois, Springer LNCS, 1988."},{"key":"1_CR14","volume-title":"Implementing circumscription using a tableau method","author":"I. Niemel\u00e4","year":"1996","unstructured":"I. Niemel\u00e4. Implementing circumscription using a tableau method. In Proceedings of the European Conference on Artificial Intelligence, Budapest, Hungary, August 1996. John Wiley. To appear."},{"key":"1_CR15","first-page":"278","volume-title":"A tableau calculus for minimal model reasoning","author":"I. Niemel\u00e4","year":"1996","unstructured":"I. Niemel\u00e4. A tableau calculus for minimal model reasoning. In Proceedings of the Fifth Workshop on Theorem Proving with Analytic Tableaux and Related Methods, pages 278\u2013294, Terrasini, Italy, May 1996. Springer-Verlag."},{"key":"1_CR16","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF00244513","volume":"4","author":"F. Oppacher","year":"1988","unstructured":"F. Oppacher and E. Suen. HARP: A Tableau-Based Theorem Prover. Journal of Automated Reasoning, 4:69\u2013100, 1988.","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR17","unstructured":"Arcot Rajasekar. Semantics for Disjunctive Logic Programs. PhD thesis, University of Maryland, 1989."},{"key":"1_CR18","first-page":"227","volume":"1","author":"J. A. Robinson","year":"1965","unstructured":"J. A. Robinson. Automated deduction with hyper-resolution. Internat. J. Comput. Math., 1:227\u2013234, 1965.","journal-title":"Internat. J. Comput. Math."},{"issue":"1","key":"1_CR19","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1016\/S0747-7171(89)80012-4","volume":"7","author":"J. H. Siekmann","year":"1989","unstructured":"J\u00f6rg H. Siekmann. Unification Theory. Journal of Symbolic Computation, 7(1):207\u2013274, January 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"G. Sutcliffe, C. Suttner, and T. Yemenis. The TPTP problem library. In A. Bundy, editor, Proc. CADE-12, volume 814 of LNAI. Springer, 1994.","DOI":"10.1007\/3-540-58156-1_18"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61630-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T12:42:05Z","timestamp":1558269725000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61630-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540616306","9783540706434"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-61630-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]},"assertion":[{"value":"2 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}