{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:08:18Z","timestamp":1725484098192},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439295"},{"type":"electronic","value":"9783540456162"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45616-3_24","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T04:26:55Z","timestamp":1179376015000},"page":"335-339","source":"Crossref","is-referenced-by-count":8,"title":["DCTP 1.2 \u2014 System Abstract"],"prefix":"10.1007","author":[{"given":"Gernot","family":"Stenz","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"P. Baumgartner, N. Eisinger, and U. Furbach. A confluent connection calculus. In Harald Ganzinger, editor, Proc. CADE-16, Trento, Italy, LNAI 1632, pages 329\u2013343. Springer, 1999.","DOI":"10.1007\/3-540-48660-7_30"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"P. Baumgartner, U. Furbach, and I. Niemel\u00e4. Hyper tableaux. In Jos\u00e9 J\u00falio Alferes et al., editors, Proc. JELIA-96: Logics in Artificial Intelligence, LNAI 1126, pp. 1\u201317, Berlin, 1996. Springer.","DOI":"10.1007\/3-540-61630-6_1"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Jean-Paul Billon. The disconnection method: a confluent integration of unification in the analytic framework. In P. Migliolo et al., editors, Proc. 5th Tableaux Workshop, LNAI 1071, pp. 110\u2013126, Berlin, 1996. Springer.","DOI":"10.1007\/3-540-61208-4_8"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"S.-J. Lee and D. Plaisted. Eliminating duplication with the hyper-linking strategy. Journal of Automated Reasoning, pp. 25\u201342, 1992.","DOI":"10.1007\/BF00247825"},{"issue":"2","key":"24_CR5","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"Reinhold Letz, Johann Schumann, Stephan Bayerl, and Wolfgang Bibel. SETHEO: A high-performance theorem prover. Journal of Automated Reasoning, 8(2):183\u2013212, 1992.","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR6","series-title":"LNAI","first-page":"381","volume-title":"Proc. IJCAR-2001, Siena, Italy","author":"R. Letz","year":"2001","unstructured":"Reinhold Letz and Gernot Stenz. DCTP: A Disconnection Calculus Theorem Prover. In Rajeev Gor\u00e9, Alexander Leitsch, and Tobias Nipkow, editors, Proc. IJCAR-2001, Siena, Italy, LNAI 2083, pp. 381\u2013385. Springer, Berlin, 2001."},{"key":"24_CR7","first-page":"142","volume-title":"Proc. LPAR 2001, Havanna, Cuba","author":"R. Letz","year":"2001","unstructured":"Reinhold Letz and Gernot Stenz. Proof and Model Generation with Disconnection Tableaux. In Andrei Voronkov, editor, Proc. LPAR 2001, Havanna, Cuba, pp. 142\u2013156. Springer, Berlin, 2001."},{"key":"24_CR8","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"}],"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\/3-540-45616-3_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T04:04:33Z","timestamp":1556424273000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45616-3_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439295","9783540456162"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-45616-3_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}