CHR: A Constructive Relevant Natural-deduction Logic Export

@article{citeulike:565339, abstract = {In this paper we develop a natural-deduction logic which is both constructive and relevant. We use a proof-theoretic argument to justify the rules of the logic. The detailed framework we use to develop our system is modeled on that used to develop Martin-Lof's Type Theory.}, author = {Leslie, Neil and Mares, Edwin D.}, booktitle = {Proceedings of Computing: The Australasian Theory Symposium (CATS) 2004}, citeulike-article-id = {565339}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/j.entcs.2003.12.011}, citeulike-linkout-1 = {http://www.sciencedirect.com/science/article/B75H1-4BRPF19-C/2/14dd4cb3f9178cc89ebed38293d1899a}, day = {16}, doi = {10.1016/j.entcs.2003.12.011}, journal = {Electronic Notes in Theoretical Computer Science}, keywords = {constructive\_logic, natural\_deduction, proof\_theory, relevant\_logic}, month = {February}, pages = {158--170}, posted-at = {2006-03-27 11:59:34}, priority = {0}, title = {CHR: A Constructive Relevant Natural-deduction Logic}, url = {http://dx.doi.org/10.1016/j.entcs.2003.12.011}, volume = {91}, year = {2004} }

TY - JOUR ID - citeulike:565339 L3 - citeulike-article-id:565339 N2 - In this paper we develop a natural-deduction logic which is both constructive and relevant. We use a proof-theoretic argument to justify the rules of the logic. The detailed framework we use to develop our system is modeled on that used to develop Martin-Lof's Type Theory. JF - Electronic Notes in Theoretical Computer Science EP - 170 TI - CHR: A Constructive Relevant Natural-deduction Logic VL - 91 T2 - Proceedings of Computing: The Australasian Theory Symposium (CATS) 2004 SP - 158 KW - constructive_logic KW - natural_deduction KW - proof_theory KW - relevant_logic AU - Leslie, Neil AU - Mares, Edwin PY - 2004/02/16/ UR - http://dx.doi.org/10.1016/j.entcs.2003.12.011 ER -