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.

• Type: Conference
• Year: 1998
• Where: TABLEAUX
• Authors: Stephan Schmitt, Christoph Kreitz
• Keywords: Artificial Intelligence, Proof Knowledge, Proof Search Process, Reconstruction Requires Knowledge, TABLEAUX 1998