کد مقاله | کد نشریه | سال انتشار | مقاله انگلیسی | نسخه تمام متن |
---|---|---|---|---|
439373 | 690540 | 2006 | 8 صفحه PDF | دانلود رایگان |

The importance of the structure of cut-formulas with respect to proof length and proof depth has been studied in various occasions. It has been illustrated that a quantifier may be more powerful than a binary connective in cut-formulas with respect to the reduction (or increase) of proof length and proof depth, and a sequence of quantifiers of the same type (existential or universal) may be less powerful than a sequence of quantifiers of alternating types. This paper provides a refined view on cut-elimination through an analysis of the structure of proofs, brings new insight into the relation between cut-formulas and short proofs, and illustrates that a mixture of quantifiers and binary connectives could be important for achieving the maximal benefit of cut-formulas for obtaining short proofs.
Journal: Theoretical Computer Science - Volume 353, Issues 1–3, 14 March 2006, Pages 63-70