Open AccessThe Role of Quantifier Alternations in Cut Elimination
Author(s) -
Philipp Gerhardy
Publication year - 2003
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v10i46.21818
Subject(s) - quantifier (linguistics) , quantifier elimination , sequent , sequent calculus , mathematics , cut elimination theorem , measure (data warehouse) , calculus (dental) , discrete mathematics , arithmetic , algorithm , computer science , mathematical proof , artificial intelligence , data mining , medicine , geometry , dentistry
Extending previous results from the author's master's thesis, subsequently published in the proceedings of CSL 2003, on the complexity of cut elimination for the sequent calculus LK, we discuss the role of quantifier alternations and develop a measure to describe the complexity of cut elimination in terms of quantifier alternations in cut formulas and contractions on such formulas.