Computer Science Logic and 8th Kurt Gödel Colloquium
Philipp Gerhardy: Refined Complexity Analysis of Cut Elimination
Welcome and News
Host Institutions
Calls and Deadlines
Social Program
Location and Venue
Colocated Events
Authors' instructions
Print current pagePrint this page
In two papers from 1991 and 1994 Zhang shows how the complexity of cut elimination depends primarily on the nesting of quantifiers in cut formulas. By studying the role of contractions in cut elimination, we can refine that analysis and show how the complexity depends on a combination of contractions and quantifier nesting. With the refined analysis the upper bound on cut elimination almost coincides with Statman's lower bound and we discuss how every non-elementary growth example must display a combination of nesting of quantifiers and contractions. Finally we discuss the role of quantifier alternations and show an elementary upper bound for the forall-and-case (resp. exists-or-case).
© 2002-2003 Kurt Gödel Society, Norbert Preining. 2003-06-04 Valid HTML 4.01! Valid CSS! Debian