Towards a clausal analysis of cut-elimination

In this paper we show that a large class of cut-elimination methods can be analyzed 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...

• Type: Journal
• Year: 2006
• Where: JSC
• Authors: Matthias Baaz, Alexander Leitsch
• Keywords: Characteristic Clause, Clause Terms, JSC 2006, Resolution Proof