Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

JSC

2006

2006

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...

Added |
13 Dec 2010 |

Updated |
13 Dec 2010 |

Type |
Journal |

Year |
2006 |

Where |
JSC |

Authors |
Matthias Baaz, Alexander Leitsch |

Comments (0)