Talks and Poster Presentations (without Proceedings-Entry):
F. Aschieri:
"Natural Deduction and Curry-Howard for Herbrand Constructive Logics";
Talk: First International Conference - Formal Structures for Computation and Deduction (FSCD),
Porto, Portugal;
2016-06-22
- 2016-06-26.
English abstract:
Dummett's logic LC is intuitionistic logic extended with Dummett's 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 Dummett's logic. We prove that our typed calculus is normalizing and show that proof terms for existentially quantified formulas reduce to a list of individual terms forming an Herbrand disjunction.
Created from the Publication Database of the Vienna University of Technology.