CERES for first-order schemata

摘要

The cut-elimination method CERES (cut-elimination by resolution) (for first-and higher order classical logic) is based on the notion of a characteristic clause set, which is extracted from an LK-proof and is always unsatisfiable. Aresolution refutation of this clause set can be used as a skeleton for a proof with atomic cuts only (atomic cut normal form). This is achieved by replacing clauses from the resolution refutation by the corresponding projections of the original proof. We present a generalization of CERES (called CERESs) to first-order proof schemata. Proof schemata are parameterized sequences of first-order proofs constructed using primitive recursive definitions. We define a schematic version of the sequent calculus, called LKS, and devise algorithms to extract schematic characteristic formulas and schematic projections from these proof schemata. We also define a schematic resolution calculus for constructing ground refutations of schemata of formulas, which can be applied to refute the schematic characteristic formulas. Finally the projection schemata and resolution schemata are plugged together and one obtains a schematic representation of proofs with only quantifier-free cuts, from which schematic Herbrand sequences can be extracted. A major benefit of CERESs is the extension of cut-elimination to inductively defined proofs: we compare CERESs with standard calculi using induction rules and demonstrate that CERESs is capable of performing cut-elimination where traditional methods fail.