Some parts of the course will be based on the following references, to be considered as further reading:
Girard, Taylor, Lafont:
Proofs and Types, Cambridge University Press.
Out of Print, pdf available
Constructive Logics Part 1: A Tutorial on Proof Systems and Typed Lambda-Calculi
Available here via ftp
Constructive Logics Part 2: Linear Logic and Proof Nets
Available here via ftp
Sara Negri and Jan Von Plato:
Structural Proof Theory, Cambridge University Press
D. Miller, G. Nadathur, F. Pfenning, A. Scedrov:
Uniform Proof as a foundation of logic programming
Annals of pure and applied logics, 1991
P.Bruscoli and A.Guglielmi:
A Tutorial on proof theoretical foundations of logic programming
Schedule of Classes in April (slots marked with * in room 2026, otherwise room E005):
|10 DS5||11 DS3||12 DS5|
|17 DS5||19 DS1+DS5||20 DS3*+DS4*+DS5*|
|24 DS5||25 DS1+DS3||26 DS5|
Schedule of Classes in May (slots marked with * in room 2026, otherwise room E005):
|2||3 DS1+DS5||4 DS3*+DS4*+DS5*|
|7 DS1+DS5||8 DS1+DS5||9||10||11|
|14 DS5*||15 DS1+DS5||16 DS1+DS4||17||18|
17/5: public holiday.
05.04.12Lecture 1Introduction to the course, motivations, references, road map. Notions of formal system, axiomatic proof system, some Hilbert-Tarski systems for propositional and classical logic. Some terminology: equivalent and strongly equivalent proof systems.
10.04.12Lecture 2 Examples and exercises on axiomatic systems.
11.04.12Lecture 3Natural Deduction in intuitionistic logic. Heyting-Brouwer-Kolmogorov approach: direct proof principle and introduction rules, inversion principles and elimination rules, open and closed assumptions. Examples of deductions and systems.
12.04.12Lecture 4Natural Deduction: Extension to classical logic. Examples of deductions. Discussion on the rules.
17.04.12Lecture 5Managing assumptions in HBK: active assumptions, vacuous discharge, unique discharge, multiple discharge of assumptions. the elimination rule for disjunction. Discussion on the adequacy of the representation. Towards sequent calculus presentation of natural deduction.
19.04.12Lecture 6 and 7Sequent calculus presentation of natural deduction: systems N_I and N_C. Examples and exercises. Comparison with HBK systems.
20.04.12Lecture 8, 9 and 10 Sequent calculus for intuitionistic and classical logic: systems G_I, G_K and LK. Examples of derivations in all systems and exercises. Comparing the proof systems for design features: 'symmetries' along the and/or and the left/right axes; axioms and structural rules; adding the cut rule. G_I with and without cut: the role of contraction in cut-elimination (equivalence of the two systems). G_I with and without cut and their relations to N_I and deductions in normal form: translations (sketch). G_C and LK: justification of their structural rules.
24.04.12Lecture 11Equivalence of LK and G_C: translations in both directions.
25.04.12Lecture 12 and 13Cut-elimination in LK. Preliminary definitions, the problem of infinite reductions with the pattern cut/contraction, the multicut. Tait-Girard reduction lemma. Considerations on complexity and bounds.
26.04.12Lecture 14Semantical Cut-elimination theorem. Applications/consequences of cut-elimination: consistency.
02.05.12Lecture 15 Consequences of cut-elimination: interpolation and Beth's definability theorem. The role of cut-elimination for automated deduction. Embedding structural rules in sequents calculus proof systems: the G_3 style of proof systems for minimal, intuitionistic, classical logic.
03.05.12Lecture 16 and 17 Between intuitionistic and classical: intermediate logics, presented from G_3. Invertibility of rules and height-prewserving inversion of rules. Extending propositional G_3ip with some laws: is admissibility of structural rules preserved? Extensions with: Excluded middle, weak exluded middle, reduction ad absurdum/stability in the atomic and general case. Extending minimal G_3mp with Dummett's law: left or right rule,atomic or general; proof theoretical properties.
04.05.12Lecture 18, 19 and 20 Introduction to Abstract Logic Programming: motivations, the rule of backchaining in LK, proof search as application of backchaining. Finite, failed and infinite computations through backchaining, seen as proof search. System MNPS. Equivalence with LK (stated and not proved), and its restriction to intuitionistic logic. Uniform provability. Examples of formulae provable and not uniformly provable. Abstract logic programming language. Examples: Horn clauses, Hereditary Harrop, Higher Order and examples of their applications.
07.05.12Lecture 21 and 22 Controlling structural rules: Introduction to Linear Logic (connectives, rules, equalities, uits, intuitive meaning of connective). Abstract Logic Programming in linear logic: System Forum and its properties. Other languages: LO, Lolli, lambda-Prolog. features in languages design adequate for concurrency: abstract data type, synchronisation, abstraction. The problem of sequentiality. Causality.
08.05.12Lecture 23 and 24 Removing the inherent sequentiality in sequent's proofs: proof nets for Multiplicative Linear Logic. Reconstructing the sequential proof from the proof net: deduction net, sequential deductions, Danos-Regnier criterion of correctness.
14.05.12Lecture 25 Towards Proof nets in deep inference. Recalling concepts and theorems from the calculous of structure on classical logic, systems SKS, SKSg, and their down-fragments, cut-elimination.
15.05.12Lecture 26 and 27 Systems MLL and MLL- in the calculus of structures; study of proof nets in deep inference, 2-sided proof nets in sequent calculus and polarities in proof nets in deep inference. Results.
16.05.12Lecture 28 and 29 Gödel incompleteness theorems.
This course has no tutors. The Open house slot is a good venue for discussing your questions, and hopefully I can answer them. Otherwise just drop me an email and we'll arrange for an appointment.
2.04.12Paola Bruscoliemail (replace AT by @)