Transforming and Analyzing Proofs in the CERES-System.
Stefan Hetzl, Alexander Leitsch, Daniel S. Weller, Bruno Woltzenlogel Paleo · 2008
Cut-elimination is the most prominent form of proof transformation in logic. The elimination of cuts in formal proofs corresponds to the removal of intermediate statements (lemmas) in mathe-matical proofs. Cut-elimination can be applied to mine real mathematical proofs, i.e. for extracting explicit and algorithmic information. The system CERES (cut-elimination by resolution) is based on automated deduction and was successfully applied to the analysis of nontrivial mathematical proofs. In this paper we focus on the input-output environment of CERES, and show how users can interact with the system and extract new mathematical knowledge. 1