  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.
