Towards a clausal analysis of cut-elimination

Citations of this article
Mendeley users who have this article in their library.
Get full text


In this paper we show that a large class of cut-elimination methods can be analysed by clause terms representing sets of characteristic clauses extractable from the original proof. Every reduction step of a cut-elimination procedure defines an operation on the corresponding clause term. Using this formal framework we prove that the methods of Gentzen and Tait and, more generally, every method based on a specific set of cut-reduction rules R, yield a resolution proof which is subsumed by a resolution proof of the characteristic clause set. As a consequence we obtain that CERES (a resolution-based method of cut-elimination) is never inferior to any method based on R. On the other hand we show that CERES is not optimal in general; instead there exist cut-reduction rules which efficiently simplify the set of characteristic clauses and thus produce much shorter proofs. Further improvements and pruning methods could thus be obtained by a structural (syntactic) analysis of the characteristic clause terms. © 2005 Elsevier Ltd. All rights reserved.




Baaz, M., & Leitsch, A. (2006). Towards a clausal analysis of cut-elimination. Journal of Symbolic Computation, 41(3–4), 381–410.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free