Deleting Redundancy in Proof Reconstruction.
Stephan Schmitt, Christoph Kreitz.
In H. de Swaart, ed., International Conference TABLEAUX-98, LNAI 1397, pp. 262-276, Springer Verlag, 1998.
Abstract
	Reconstructing sequent proofs from matrix proofs in non-classical logics requires the elimination of redundancies in order retain completeness when a proof branches into independent sub-proofs, which is a non-trivial task if additional search shall be avoided. We present a framework for eliminating redundancies during proof reconstruction. We show that search-free proof reconstruction requires knowledge from the proof search process. We relate different levels of proof knowledge to reconstruction knowledge and analyze which redundancies can be deleted by using such knowledge. Our framework is uniformly applicable to all logics which have a matrix-characterization of validity and enables us to build adequate conversion procedures for each logic.

		Paper is available in postscript and pdf format		Slides of the conference presentation are available in compressed postscript and pdf format (Presentation: Stephan Schmitt)
Bibtex Entry					Back to overview of papers
	@InProceedings{inp:SchmittKreitz98a, author = "Stephan Schmitt and Christoph Kreitz", title = "Deleting Redundancy in Proof Reconstruction", booktitle = "International Conference TABLEAUX-98", year = "1998", editor = "H. de~Swaart", volume = "1397", series = LNAI, pages = "262--276", publisher = SPRINGER }