Comparing the Complexity of Cut-Elimination Methods Export

@incollection{citeulike:1743808, abstract = {We investigate the relative complexity of two different methods of cut-elimination in classical first-order logic, namely the methods of Gentzen and Tait. We show that the methods are incomparable, in the sense that both can give a nonelementary speed-up of the other one. More precisely we construct two different sequences of LK-proofs with cuts where cut-elimination for one method is elementary and nonelementary for the other one. Moreover we show that there is also a nonelementary difference in complexity for different deterministic versions of Gentzen's method.}, author = {Baaz, Matthias and Leitsch, Alexander}, citeulike-article-id = {1743808}, citeulike-linkout-0 = {http://www.springerlink.com/content/8d0qnkh7tjj63uxv}, journal = {Proof Theory in Computer Science: International Seminar, PTCS 2001 Dagstuhl Castle, Germany, October 7-12, 2001, Proceedings}, keywords = {proof\_theory}, pages = {49+}, posted-at = {2007-10-09 00:56:07}, priority = {5}, title = {Comparing the Complexity of Cut-Elimination Methods}, url = {http://www.springerlink.com/content/8d0qnkh7tjj63uxv}, year = {2001} }

TY - CHAP ID - citeulike:1743808 L3 - citeulike-article-id:1743808 N2 - We investigate the relative complexity of two different methods of cut-elimination in classical first-order logic, namely the methods of Gentzen and Tait. We show that the methods are incomparable, in the sense that both can give a nonelementary speed-up of the other one. More precisely we construct two different sequences of LK-proofs with cuts where cut-elimination for one method is elementary and nonelementary for the other one. Moreover we show that there is also a nonelementary difference in complexity for different deterministic versions of Gentzen's method. JF - Proof Theory in Computer Science: International Seminar, PTCS 2001 Dagstuhl Castle, Germany, October 7-12, 2001, Proceedings TI - Comparing the Complexity of Cut-Elimination Methods SP - 49 KW - proof_theory AU - Baaz, Matthias AU - Leitsch, Alexander PY - 2001/// UR - http://www.springerlink.com/content/8d0qnkh7tjj63uxv ER -