B. Woltzenlogel-Paleo:

"A Deep Natural Deduction Calculus";

Talk: 2nd Workshop Structural Proof Theory, Innsbruck (invited); 2011-10-26 - 2011-10-29.

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.

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.

Proof Theory, Natural Deduction, Deep Inference, Proof Compression

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