{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:26:27Z","timestamp":1725549987969},"publisher-location":"Berlin, Heidelberg","reference-count":5,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540289319"},{"type":"electronic","value":"9783540318224"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11554554_24","type":"book-chapter","created":{"date-parts":[[2005,9,27]],"date-time":"2005-09-27T14:02:57Z","timestamp":1127829777000},"page":"312-317","source":"Crossref","is-referenced-by-count":0,"title":["Proof Output and Transformation for Disconnection Tableaux"],"prefix":"10.1007","author":[{"given":"Philipp","family":"Correll","sequence":"first","affiliation":[]},{"given":"Gernot","family":"Stenz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3","key":"24_CR1","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\u2013338 (1994)","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","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, vol.\u00a02250, pp. 142\u2013156. Springer, Heidelberg (2001)"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","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, vol.\u00a02381, pp. 176\u2013190. Springer, Heidelberg (2002)"},{"key":"24_CR4","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/BF00244513","volume":"4","author":"F. Oppacher","year":"1988","unstructured":"Oppacher, F., Suen, E.: HARP: A tableau-based theorem prover. Journal of Automated Reasoning\u00a04, 69\u2013100 (1988)","journal-title":"Journal of Automated Reasoning"},{"key":"24_CR5","unstructured":"Stenz, G.: The Disconnection Calculus. Logos Verlag, Berlin (2002), Dissertation, Fakult\u00e4t f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen"}],"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\/11554554_24.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:06:50Z","timestamp":1619507210000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11554554_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540289319","9783540318224"],"references-count":5,"URL":"https:\/\/doi.org\/10.1007\/11554554_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}