[Back]


Talks and Poster Presentations (without Proceedings-Entry):

B. Woltzenlogel-Paleo:
"A Deep Natural Deduction Calculus";
Talk: 2nd Workshop Structural Proof Theory, Innsbruck (invited); 2011-10-26 - 2011-10-29.



English abstract:
In this talk I will describe an extension of the natural deduction
calculus (for the purely implicative fragment of intuitionistic logic
only) that allows inference rules to be applied deeply. I will discuss
the following:
1) (Mostly technological) motivations for the development of this calculus.
2) Soundness and completeness relative to the standard (shallow)
natural deduction calculus will be displayed.
3) A "deep lambda calculus" whose terms correspond to deep natural
deduction proofs (a la Curry-Howard).
4) Normalization and beta-reduction.
5) Proof compression by translating from shallow to deep natural deduction.

German abstract:
In this talk I will describe an extension of the natural deduction
calculus (for the purely implicative fragment of intuitionistic logic
only) that allows inference rules to be applied deeply. I will discuss
the following:
1) (Mostly technological) motivations for the development of this calculus.
2) Soundness and completeness relative to the standard (shallow)
natural deduction calculus will be displayed.
3) A "deep lambda calculus" whose terms correspond to deep natural
deduction proofs (a la Curry-Howard).
4) Normalization and beta-reduction.
5) Proof compression by translating from shallow to deep natural deduction.

Keywords:
Proof Theory, Natural Deduction, Deep Inference, Proof Compression

Created from the Publication Database of the Vienna University of Technology.