Future Work
We plan to develop the following extensions of CERES:
- Analysis of the relation between CERES and reductive methods. This may enable us to combine the good traits from each method and to orient CERES toward specific normal forms.
- Enabling a full automation of CERESω. Right now, due to lack of sufficiently strong higher order theorem prover, the refutation of higher order characteristic clause sets cannot be done automatically. We work on finding algorithms that can refute subclasses of problems in higher order logic, most notably second order arithmetic.
- The studying of invariance properties of proofs in order to prove that cut elimination is independant of the syntactic representations of proofs.
- The study of CERES in intuitionistic logic.
- We plan to develop algorithms for computing interpolants, which allow the replacement of implicit definitions by explicit ones according to Beth's Theorem.
- 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.
- The implementation of CERESω lead to a complete rewrite of the CERES system based on simply typed lambda calculus which is still in progress. As long as some features are only available in the old system, both will be maintained simultaneously.
- We are currently introducing the CERES method to a schematized sequent calculus in a joint project with the Laboratory of Informatics of Grenoble. At the moment we are working on propositional schemas defined via prmitive recursion. In the future we will also look into first order schemas.