Title: Clausal Analysis of First-order Proof Schemata,
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.