Sciweavers

JSC
2006

Towards a clausal analysis of cut-elimination

13 years 10 months ago
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...
Matthias Baaz, Alexander Leitsch
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2006
Where JSC
Authors Matthias Baaz, Alexander Leitsch
Comments (0)