CHR: A Constructive Relevant Natural-deduction Logic
Neil Leslie, EDWIN D. MARES · Electronic Notes in Theoretical Computer Science · 2004
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-Löf's Type Theory.