Sciweavers

Share
TABLEAUX
1998
Springer

Deleting Redundancy in Proof Reconstruction

11 years 5 months ago
Deleting Redundancy in Proof Reconstruction
We present a framework for eliminating redundancies during the reconstruction of sequent proofs from matrix proofs. 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 classical logic and all non-classical logics which have a matrix characterization of validity and enables us to build adequate conversion procedures for each logic.
Stephan Schmitt, Christoph Kreitz
Added 06 Aug 2010
Updated 06 Aug 2010
Type Conference
Year 1998
Where TABLEAUX
Authors Stephan Schmitt, Christoph Kreitz
Comments (0)
books