Towards a clausal analysis of cut-elimination

  • Baaz M
  • Leitsch A
  • 4


    Mendeley users who have this article in their library.
  • 20


    Citations of this article.


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.

Author-supplied keywords

  • Clause terms
  • Cut-elimination
  • Resolution

Get free article suggestions today

Mendeley saves you time finding and organizing research

Sign up here
Already have an account ?Sign in

Find this document


  • Matthias Baaz

  • Alexander Leitsch

Cite this document

Choose a citation style from the tabs below

Save time finding and organizing research with Mendeley

Sign up for free