Mismatch Export

@unpublished{citeulike:5853065, abstract = {There is a mismatch between meta and object levels in many calculi, like the sequent calculus and natural deduction. The mismatch has undesirable proof theoretical consequences, the most important being the inability to design deductive systems. Since the object level is untouchable (it's the language you want to deal with), one can fix the problem by `improving ́ the meta level; or one can also sort of merge object and meta level by using deep inference.}, author = {Guglielmi, Alessio}, citeulike-article-id = {5853065}, citeulike-linkout-0 = {http://iccl.tu-dresden.de/~guglielm/p/AG9.pdf}, day = {24}, keywords = {display-logic, inference, linear-logic, logical-frameworks, metatheory, mismatch, natural-deduction}, month = {March}, posted-at = {2009-09-29 18:50:42}, priority = {0}, school = {TU Dresden}, title = {Mismatch}, url = {http://iccl.tu-dresden.de/~guglielm/p/AG9.pdf}, year = {2003} }

TY - UNPB ID - citeulike:5853065 L3 - citeulike-article-id:5853065 N2 - There is a mismatch between meta and object levels in many calculi, like the sequent calculus and natural deduction. The mismatch has undesirable proof theoretical consequences, the most important being the inability to design deductive systems. Since the object level is untouchable (it's the language you want to deal with), one can fix the problem by `improving ́ the meta level; or one can also sort of merge object and meta level by using deep inference. TI - Mismatch KW - display-logic KW - inference KW - linear-logic KW - logical-frameworks KW - metatheory KW - mismatch KW - natural-deduction AU - Guglielmi, Alessio PY - 2003/03/24/ UR - http://iccl.tu-dresden.de/~guglielm/p/AG9.pdf ER -