Structure of proofs and the complexity of cut elimination Export

@article{citeulike:519758, abstract = {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.}, author = {Zhang, Wenhui}, citeulike-article-id = {519758}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/j.tcs.2005.07.042}, citeulike-linkout-1 = {http://www.sciencedirect.com/science/article/B6V1G-4HHPBRW-2/2/622fa8dd49978337eec391559befea1e}, day = {14}, doi = {10.1016/j.tcs.2005.07.042}, journal = {Theoretical Computer Science}, keywords = {calculus, cut\_elimination, logic, pnc, proof, sequent, structure}, month = {March}, number = {1-3}, pages = {63--70}, posted-at = {2006-02-24 12:28:40}, priority = {2}, title = {Structure of proofs and the complexity of cut elimination}, url = {http://dx.doi.org/10.1016/j.tcs.2005.07.042}, volume = {353}, year = {2006} }

TY - JOUR ID - citeulike:519758 L3 - citeulike-article-id:519758 N2 - 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. IS - 1-3 JF - Theoretical Computer Science EP - 70 TI - Structure of proofs and the complexity of cut elimination VL - 353 SP - 63 KW - calculus KW - cut_elimination KW - logic KW - pnc KW - proof KW - sequent KW - structure AU - Zhang, Wenhui PY - 2006/03/14/ UR - http://dx.doi.org/10.1016/j.tcs.2005.07.042 ER -