CERES in higher-order logic

Abstract

We define a generalization of the first-order cut-elimination method CERES to higher-order logic. At the core of lies the computation of an (unsatisfiable) set of sequents (the characteristic sequent set) from a proof of a sequent . A refutation of in a higher-order resolution calculus can be used to transform cut-free parts of (the proof projections) into a cut-free proof of . An example illustrates the method and shows that can produce meaningful cut-free proofs in mathematics that traditional cut-elimination methods cannot reach.