Future Work
We plan to develop the following extensions of CERES:
- We plan to develop algorithms 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 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.