Cut elimination for the second order propositional logic with Hilbert's ε-symbol, extensionality, and full comprehension Export

@incollection{citeulike:1743119, abstract = {The cut-elimination technique is well developed for classical higher order systems, but, since the normal form (not normalization) theorem was established by Mints[1, 2, 3, 4, 5], not much further progress has been achieved for the logical systems with an ε-symbol.}, author = {Gavrilovich, Michael}, citeulike-article-id = {1743119}, citeulike-linkout-0 = {http://dx.doi.org/10.1007/3-540-63045-7_12}, doi = {10.1007/3-540-63045-7_12}, journal = {Logical Foundations of Computer Science}, keywords = {epsilon, proof\_theory, sequent\_calculus}, pages = {113--118}, posted-at = {2007-10-08 20:01:15}, priority = {4}, title = {Cut elimination for the second order propositional logic with Hilbert's ε-symbol, extensionality, and full comprehension}, url = {http://dx.doi.org/10.1007/3-540-63045-7_12}, year = {1997} }

TY - CHAP ID - citeulike:1743119 L3 - citeulike-article-id:1743119 N2 - The cut-elimination technique is well developed for classical higher order systems, but, since the normal form (not normalization) theorem was established by Mints[1, 2, 3, 4, 5], not much further progress has been achieved for the logical systems with an ε-symbol. JF - Logical Foundations of Computer Science EP - 118 TI - Cut elimination for the second order propositional logic with Hilbert's ε-symbol, extensionality, and full comprehension SP - 113 KW - epsilon KW - proof_theory KW - sequent_calculus AU - Gavrilovich, Michael PY - 1997/// UR - http://dx.doi.org/10.1007/3-540-63045-7_12 ER -