{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T18:51:36Z","timestamp":1725475896613},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676973"},{"type":"electronic","value":"9783540450085"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722086_31","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T19:43:15Z","timestamp":1167421395000},"page":"398-414","source":"Crossref","is-referenced-by-count":2,"title":["A Tableau-Like Representation Framework for Efficient Proof Reconstruction"],"prefix":"10.1007","author":[{"given":"Stephan","family":"Schmitt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"31_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/3-540-10009-1_22","volume-title":"5th Conference on Automated Deduction","author":"P.B. Andrews","year":"1980","unstructured":"Andrews, P.B.: Transforming matings into natural deduction proofs. In: Bibel, W. (ed.) CADE 1980. LNCS, vol.\u00a087, pp. 281\u2013292. Springer, Heidelberg (1980)"},{"issue":"3","key":"31_CR2","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/BF00881804","volume":"15","author":"B. Beckert","year":"1995","unstructured":"Beckert, B., Posegga, J.: leanTAP: Lean tableau-based deduction. Journal of Automated Reasoning\u00a015(3), 339\u2013358 (1995)","journal-title":"Journal of Automated Reasoning"},{"key":"31_CR3","doi-asserted-by":"crossref","unstructured":"Bibel, W.: Automated theorem proving, Vieweg, Braunschweig (1982)","DOI":"10.1007\/978-3-322-90100-2"},{"key":"31_CR4","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"783","DOI":"10.1007\/3-540-58156-1_60","volume-title":"Automated Deduction - CADE-12","author":"W. Bibel","year":"1994","unstructured":"Bibel, W., Br\u00fcning, S., Egly, U., Rath, T.: Komet. In: Bundy, A. (ed.) CADE 1994. LNCS (LNAI), vol.\u00a0814, pp. 783\u2013787. Springer, Heidelberg (1994)"},{"key":"31_CR5","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-49674-2_1","volume-title":"Logic Program Synthesis and Transformation","author":"W. Bibel","year":"1998","unstructured":"Bibel, W., Korn, D., Kreitz, C., Kurucz, F., Otten, J., Schmitt, S., Stolpmann, G.: A multi-level approach to program synthesis. In: Fuchs, N.E. (ed.) LOPSTR 1997. LNCS (LNAI), vol.\u00a01463, pp. 1\u201325. Springer, Heidelberg (1998)"},{"key":"31_CR6","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Design and Implementation of Symbolic Computation Systems","author":"W. Bibel","year":"1996","unstructured":"Bibel, W., Korn, D., Kreitz, C., Schmitt, S.: Problem-oriented applications of automated theorem proving. In: Limongelli, C., Calmet, J. (eds.) DISCO 1996. LNCS, vol.\u00a01128, pp. 1\u201321. Springer, Heidelberg (1996)"},{"key":"31_CR7","volume-title":"Implementing mathematics with the NuPRL proof development system","author":"R. Constable","year":"1986","unstructured":"Constable, R., et al.: Implementing mathematics with the NuPRL proof development system. Prentice Hall, Englewood Cliffs (1986)"},{"key":"31_CR8","unstructured":"Dahn, B.I., et al.: Integrating logical functions with ILF. Preprint 94-10, Humboldt Universit\u00e4t zu Berlin (1994)"},{"key":"31_CR9","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-48660-7_10","volume-title":"Automated Deduction - CADE-16","author":"H. Horacek","year":"1999","unstructured":"Horacek, H.: Presenting proofs in a human-oriented way. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 142\u2013156. Springer, Heidelberg (1999)"},{"key":"31_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"399","DOI":"10.1007\/3-540-61532-6_34","volume-title":"PRICAI \u201996: Topics in Artificial Intelligence","author":"X. Huang","year":"1996","unstructured":"Huang, X.: Translating machine-generated resolution proofs into ND-proofs at the assertion level. In: Foo, N.Y., G\u00f6bel, R. (eds.) PRICAI 1996. LNCS, vol.\u00a01114, pp. 399\u2013410. Springer, Heidelberg (1996)"},{"key":"31_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-017-2794-5","volume-title":"Proof methods for modal and intuitionistic logic","author":"M.C. Fitting","year":"1983","unstructured":"Fitting, M.C.: Proof methods for modal and intuitionistic logic. D. Reidel, Dordrechtz (1983)"},{"key":"31_CR12","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/3-540-63104-6_20","volume-title":"Automated Deduction - CADE-14","author":"C. Kreitz","year":"1997","unstructured":"Kreitz, C., Mantel, H., Otten, J., Schmitt, S.: Connection-based proof construction in linear logic. In: McCune, W. (ed.) CADE 1997. LNCS (LNAI), vol.\u00a01249, pp. 207\u2013221. Springer, Heidelberg (1997)"},{"issue":"3","key":"31_CR13","first-page":"88","volume":"5","author":"C. Kreitz","year":"1999","unstructured":"Kreitz, C., Otten, J.: Connection-based theorem proving in classical and nonclassical logics. Journal for Universal Computer Science\u00a05(3), 88\u2013112 (1999)","journal-title":"Journal for Universal Computer Science"},{"key":"31_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/3-540-60939-3_10","volume-title":"Logic Program Synthesis and Transformation","author":"C. Kreitz","year":"1996","unstructured":"Kreitz, C., Otten, J., Schmitt, S.: Guiding program development systems by a connection based proof strategy. In: Proietti, M. (ed.) LOPSTR 1995. LNCS, vol.\u00a01048, pp. 137\u2013151. Springer, Heidelberg (1996)"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"Kreitz, C., Schmitt, S.: A uniform procedure for converting matrix proofs into sequent-style systems. Journal of Information and Computation (2000) (to appear)","DOI":"10.1006\/inco.2000.2913"},{"key":"31_CR16","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/BF00244282","volume":"8","author":"R. Letz","year":"1992","unstructured":"Letz, R., Schumann, J., Bayerl, S., Bibel, W.: Setheo: A high-performance theorem prover. Journal of Automated Reasoning\u00a08, 183\u2013212 (1992)","journal-title":"Journal of Automated Reasoning"},{"key":"31_CR17","volume-title":"IJCAI 1989","author":"C. Lingenfelder","year":"1989","unstructured":"Lingenfelder, C.: Structuring computer generated proofs. In: IJCAI 1989. Morgan Kaufmann, San Francisco (1989)"},{"key":"31_CR18","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-49545-2_12","volume-title":"Logics in Artificial Intelligence","author":"H. Mantel","year":"1998","unstructured":"Mantel, H., Kreitz, C.: A matrix characterization for MELL. In: Dix, J., Fari\u00f1as del Cerro, L., Furbach, U. (eds.) JELIA 1998. LNCS (LNAI), vol.\u00a01489, pp. 169\u2013183. Springer, Heidelberg (1998)"},{"key":"31_CR19","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-48754-9_20","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"H. Mantel","year":"1999","unstructured":"Mantel, H., Otten, J.: linTAP: A tableau prover for linear logic. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol.\u00a01617, pp. 217\u2013231. Springer, Heidelberg (1999)"},{"key":"31_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1007\/BFb0047132","volume-title":"7th International Conference on Automated Deduction","author":"D.A. Miller","year":"1984","unstructured":"Miller, D.A.: Expansion tree proofs and their conversion to natural deduction proofs. In: Shostak, R.E. (ed.) CADE 1984. LNCS, vol.\u00a0170, pp. 375\u2013393. Springer, Heidelberg (1984)"},{"key":"31_CR21","unstructured":"Ohlbach, H.J.: A resolution calculus for modal logics. PhD Thesis, Univ. Kaiserslautern (1988)"},{"key":"31_CR22","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0027422","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"J. Otten","year":"1997","unstructured":"Otten, J.: ileanTAP: An intuitionistic theorem prover. In: Galmiche, D. (ed.) TABLEAUX 1997. LNCS (LNAI), vol.\u00a01227, pp. 307\u2013386. Springer, Heidelberg (1997)"},{"key":"31_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/BFb0047133","volume-title":"7th International Conference on Automated Deduction","author":"F. Pfenning","year":"1984","unstructured":"Pfenning, F.: Analytic and non-analytic proofs. In: Shostak, R.E. (ed.) CADE 1984. LNCS, vol.\u00a0170, pp. 394\u2013413. Springer, Heidelberg (1984)"},{"key":"31_CR24","unstructured":"Pfenning, F.: Proof transformations in higher-order logic. Ph.D. Thesis. Carnegie Mellon University, Pittsburgh (1987)"},{"issue":"1","key":"31_CR25","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J.A. Robinson","year":"1965","unstructured":"Robinson, J.A.: A machine-oriented logic based on the resolution principle. Journal of the ACM\u00a012(1), 23\u201341 (1965)","journal-title":"Journal of the ACM"},{"key":"31_CR26","unstructured":"Schmitt, S.: Proof reconstruction in classical and non-classical logics. PhD Thesis, TU-Darmstadt (1999)"},{"key":"31_CR27","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"106","DOI":"10.1007\/3-540-59338-1_31","volume-title":"Theorem Proving with Analytic Tableaux and Related Methods","author":"S. Schmitt","year":"1995","unstructured":"Schmitt, S., Kreitz, C.: On transforming intuitionistic matrix proofs into standardsequent proofs. In: Baumgartner, P., Posegga, J., H\u00e4hnle, R. (eds.) TABLEAUX 1995. LNCS (LNAI), vol.\u00a0918, pp. 106\u2013121. Springer, Heidelberg (1995)"},{"key":"31_CR28","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"418","DOI":"10.1007\/3-540-61511-3_104","volume-title":"Automated Deduction - Cade-13","author":"S. Schmitt","year":"1996","unstructured":"Schmitt, S., Kreitz, C.: Converting non-classical matrix proofs into sequent-style systems. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104, pp. 418\u2013432. Springer, Heidelberg (1996)"},{"key":"31_CR29","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-69778-0_27","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"S. Schmitt","year":"1998","unstructured":"Schmitt, S., Kreitz, C.: Deleting Redundancy in proof reconstruction. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, pp. 262\u2013276. Springer, Heidelberg (1998)"},{"key":"31_CR30","volume-title":"Automated deduction in non-classical logics","author":"L. Wallen","year":"1990","unstructured":"Wallen, L.: Automated deduction in non-classical logics. MIT Press, Cambridge (1990)"},{"key":"31_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1007\/3-540-52885-7_109","volume-title":"10th International Conference on Automated Deduction","author":"L. Wos","year":"1990","unstructured":"Wos, L., et al.: Automated reasoning contributes to mathematics and logic. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol.\u00a0449, pp. 485\u2013499. Springer, Heidelberg (1990)"}],"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\/10722086_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T05:43:11Z","timestamp":1553319791000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/10722086_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}