On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC

Logical Methods in Computer Science, Volume abs/1609.03190, 2017.

Cited by: 6|Bibtex|Views1|Links
EI

Abstract:

Dummettu0027s logic LC is intuitionistic logic extended with Dummettu0027s axiom: for every two statements the first implies the second or the second implies the first. We present a natural deduction and a Curry-Howard correspondence for first-order and second-order Dummettu0027s logic. We add to the lambda calculus an operator which repr...More

Code:

Data:

Your rating :
0

 

Tags
Comments