Vorträge und Posterpräsentationen (ohne Tagungsband-Eintrag):
B. Woltzenlogel-Paleo:
"A Deep Natural Deduction Calculus";
Vortrag: 2nd Workshop Structural Proof Theory,
Innsbruck (eingeladen);
26.10.2011
- 29.10.2011.
Kurzfassung deutsch:
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.
Kurzfassung englisch:
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.
Schlagworte:
Proof Theory, Natural Deduction, Deep Inference, Proof Compression
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.