Lehrveranstaltungsleiter: Alexander Leitsch
The project is obligatory part of the International Master Study Computational Logic.
First Meeting:
Monday, October 5 2009, 13:15
Zemanek-Hörsaal,
Favoritenstrasse 9, ground floor
CONTENT:
Programming and Experiments with the system CERES
CERES (= cut-elimination by resolution) is a system for automated proof transformation, in particular for cut-elimination in real mathematical proofs. The core of the cut-elimination procedure is a clausal theorem prover; this prover is used to refute the so-called characteristic clause set which contains the essence of the original proof. The resolution refutation obtained by the prover represents the skeleton of a cut-free proof and contains the key for constructions and algorithms corresponding to the new cut-free proof. As the characteristic clause sets typically contain complex mathematical information, current theorem provers frequently fail to refute the set. Therefore it is desirable to develop more efficient theorem proving methods for the needs of CERES. The purpose of this project is the further development of the theorem proving environment of CERES; this includes the development and programming of specific algorithms and heuristics, the comparison of different theorem provers, and their evaluation w.r.t. CERES.
A.Leitsch