Future Work
We plan to develop the following extensions of CERES:
- As the cut-free proofs are often very large and difficult to interpret, we intend to provide the possibility to analyze certain characteristics of the cut-free proof (which are simpler than the proof itself). An important example are Herbrand sequents which may serve to extract bounds from proofs (see e.g. Luckhardt 1989). We plan to develop algorithms for extracting Herbrand sequents (also from proofs of nonprenex sequents as indicated in Baaz and Leitsch 1994) and for computing interpolants, which allow for the replacement of implicit definitions by explicit ones according to Beth's Theorem.
- The current method CERES eliminates all cuts at once. This is necessary as projections are only possible to skolemized sequents, and cuts or ancestors of cuts cannot be skolemized. To make elimination of single cuts possible, we plan to develop a specific resolution calculus without skolemization, in which the characteristic clause set of non-skolemized proofs can be refuted directly. In this new calculus also the concept of projection has to be revised.
- A serious defect of the current method is that it cannot handle inductive proofs. Clearly cut-elimination in inductive proofs is very problematic already in theory. But there are some restricted systems which deserve investigation. One candidate is ACA0 (see Simpson 1999), a weak second-order system of arithmetic with first-order comprehension; the LK-axioms in such proofs are ordinary first-order clauses. This opens the way for extending CERES to induction (but also here skolemization has to be avoided).
- A great challenge in the formal analysis of mathematical proofs lies in providing a suitable format for input and output of proofs. We plan to improve our intermediary proof language and to move closer to the "natural" language of mathematical proofs.
To demonstrate the abilities of CERES and the feasibility of formalizing and analyzing complex proofs of mathematical relevance, we currently investigate Fürstenberg's well known proof of the infinity of primes using topology (which may be found in "Proofs from THE BOOK"). The refutations of the characteristic clause set of the problem reflected some of the well-known prime constructions (in particular also Euclid's one).