CERES for First-Order Schemata

Abstract

The cut-elimination method CERES (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. A resolution 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 and define a schematic version of the sequent calculus called LKS, and a notion of proof schema based on primitive recursive definitions. A method is developed to extract schematic characteristic clause sets and schematic projections from these proof schemata. We also define a schematic resolution calculus for refutation of schemata of clause sets, which can be applied to refute the schematic characteristic clause sets. Finally the projection schemata and resolution schemata are plugged together and a schematic representation of the atomic cut normal forms is obtained. 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. The algorithmic handling of CERESs is supported by a recent extension of the CERES system.