Clausal Analysis of First-order Proof Schemata
From MaRDI portal
Publication:6282945
DOI10.1109/SYNASC.2017.00029arXiv1702.02589MaRDI QIDQ6282945FDOQ6282945
Authors: David M. Cerna, Michael Peter Lettmann 
Publication date: 8 February 2017
Abstract: Proof schemata are a variant of LK-proofs able to simulate various induction schemes in first-order logic by adding so called proof links to the standard first-order LK-calculus. Proof links allow proofs to reference proofs thus giving proof schemata a recursive structure. Unfortunately, applying reductive cut- elimination is non-trivial in the presence of proof links. Borrowing the concept of lazy instantiation from functional programming, we evaluate proof links locally allowing reductive cut-elimination to proceed past them. Though, this method cannot be used to obtain cut-free proof schemata, we nonetheless obtain important results concerning the schematic CERES method, that is a method of cut-elimination for proof schemata based on resolution. In "Towards a clausal analysis of cut-elimination", it was shown that reductive cut-elimination transforms a given LK-proof in such a way that a subsumption relation holds between the pre- and post-transformation characteristic clause sets, i.e. the clause set representing the cut-structure of an LK-proof. Let CL(A') be the characteristic clause set of a normal form A' of an LK-proof A that is reached by performing reductive cut-elimination on A without atomic cut elimination. Then CL(A') is subsumed by all characteristic clause sets extractable from any application of reductive cut-elimination to A. Such a normal form is referred to as an ACNF top and plays an essential role in methods of cut-elimination by resolution. These results can be extended to proof schemata through our "lazy instantiation" of proof links, and provides an essential step toward a complete cut-elimination method for proof schemata.
This page was built for publication: Clausal Analysis of First-order Proof Schemata
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6282945)
