Proof Transformation by Resolution

While automated theorem proving and the automatizing of proof search is an old and very important area in computational logic and artificial intelligence, methods of automated proof transformations received much less attention. But some of these methods, in particular cut-elimination, are of central importance in extracting mathematical and computational information from mathematical proofs. The method CERES (cut-elimination by resolution), developed by M. Baaz and the author in the late nineties, reduces the problem of cut-elimination to the refutation of a set of clauses by resolution. The logical problem of cut-elimination then becomes a matter of automated deduction and proof search. CERES is indeed a method of proof search performing proof transformations. The main aim of this project is to show that CERES is not just some method of cut-elimination, but a theoretical tool to simulate and analyze a large class of proof transformation methods. The analysis should lead to a better understanding and to improvements of several traditional methods of cut-elimination. In parallel to these theoretical investigations we plan to implement CERES and to extend it in the following ways: 1. by introducing refinements and deletion methods and 2. by transforming the method into a tool for interactive proof transformation. The final step should be an application of the new method to real mathematical proofs. We are also interested in attacking some substantial proof theoretical problems connected with CERES; one of them is the problem of re- skolemization of proofs in polynomial time.