## Introduction

Proof analysis is a central mathematical activity which proved crucial to the development of mathematics. Indeed many mathematical concepts such as the notion of group or the notion of probability were introduced by analyzing existing arguments. In some sense the analysis and synthesis of proofs form the very core of mathematical progress (see e.g. Polya 1954a and Polya 1954b).

Cut-elimination, introduced by Gentzen,
is the most prominent form of proof transformation in logic and plays an
important role in automating the analysis of mathematical proofs.
The removal of cuts corresponds to the elimination of intermediate
statements (lemmas) from proofs resulting in a proof which is
analytic in the sense, that all statements in the proof are
subformulas of the result. Therefore, the proof of a *
combinatorial statement* is converted into a purely *
combinatorial proof*. Cut-elimination is therefore an essential
tool for analyzing mathematical proofs, especially to make
implicit parameters explicit. In particular, cut free derivations
admit the extraction of Herbrand disjunctions, which can be used
for establishing bounds on existential quantifiers (e.g. see
Luckhardt's analysis of the Theorem of Roth).

In a formal sense Girard's famous analysis of van der Waerden's theorem consists in the application of cut-elimination to the proof of Fürstenberg/Weiss (which uses topological arguments) with the "perspective" of obtaining van der Waerden's elementary proof. Indeed, an application of a complex proof transformation like cut-elimination by humans requires a goal oriented strategy.

Note that cut-elimination is *non-unique*, i.e. there is no
single cut-free proof which represents *the* analytic version
of a proof with lemmas. Therefore the application of purely
computational methods on existing proofs potentially produces new
interesting proofs. Indeed, it is non-uniqueness which makes
computational experiments with cut-elimination interesting (see
Baaz, Hetzl, Leitsch, Richter and Spohr 2004).
The experiments can be considered as a source for a base of proofs in
formal format which provide different mathematical and
computational information.

CERES (see Baaz and Leitsch 2000 and
Baaz and Leitsch 2006) is a
cut-elimination method that is based on resolution. The method
roughly works as follows: The structure of the proof containing
cuts is mapped to an unsatisfiable set of clauses C
(the *characteristic clause set*). A resolution refutation of
C, which is obtained using a first-order theorem
prover, serves as a skeleton for the new proof which contains only atomic
cuts. In a final step also these atomic cuts can be eliminated, provided the
(atomic) axioms are valid sequents; but this step is of minor
mathematical interest and of low complexity. In the system
CERES this method of cut-elimination has been implemented. The system is
capable of dealing with formal proofs in an extended version of
**LK**, among them also very large ones (i.e. proofs with more
than 1500 nodes and cut-elimination has been done within 14 seconds).
The extension of CERES from **LK** to **LKDe**,
a calculus containing definition introductions and equality rules (see
Leitsch and Richter 2005 and
Baaz, Hetzl, Leitsch, Richter and Spohr 2006),
moves the system closer to real mathematical proofs.

Another step is the extension of CERES to second and higher order logic (see Hetzl, Leitsch, Weller and Woltzenlogel Paleo 2009, Weller 2010 and Hetzl, Leitsch and Weller 2011). Since proof Skolemization does not carry over to higher order logic, eigenvariables are replaced by Skolem terms in the sequent calculus **LK _{sk}**. Now the proof projections may become locally unsound due to eigenvariable violations, still they fulfill some global soundness conditions which allows to transform them back to

**LK**. The system CERES was extended within the Generic architecture for proofs framework in order to support these features.

An alternative approach to higher order logic is the extension of CERES to a schematic sequent calculus **LK _{sch}** defined by primitve recursion. In the first step, a restricted class of cuts over propositional proofs is analyzed. The next goal is the generalization to first order formulas. Research in this direction is undertaken in a joint project with the CAPP at the Laboratoire d'Informatique de Grenoble.