[Back]

A. Lolic:
"Extraction of expansion trees using CERES";
Talk: The Fine Structure of Formal Proof Systems and their Computational Interpretations - FISP, Innsbruck; 2016-11-14 - 2016-11-18.

We define a new method for proof mining by CERES that is concerned with the extraction of expansion trees. In the original CERES method expansion trees can be extracted from proofs in normal form (proofs without quantified cuts) as a post-processing of cut-elimination. More precisely they are extracted from an ACNF, a proof with at most atomic cuts. We define a novel method avoiding proof normalization and show that expansion trees can be extracted from the resolution refutation and the corresponding proof projections. We prove that the new method asymptotically outperforms the standard method (which first computes the ACNF and then extracts the expansion tree).

cut-elimination, expansion tree, Herbrand sequent, automated deduction