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

Jean Gallier:

Constructive Logics Part 1: A Tutorial on Proof Systems and Typed Lambda-Calculi

Available here via ftp

Jean Gallier:

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

ISBN 0-521-79307-6

D. Miller, G. Nadathur, F. Pfenning, A. Scedrov:

Uniform Proof as a foundation of logic programming

Annals of pure and applied logics, 1991

Available here

P.Bruscoli and A.Guglielmi:

A Tutorial on proof theoretical foundations of logic programming

ICLP 2003

Available here.

- In principle, all what has been covered and is listed in Lectures and Topics.
- Modality of exam:
**Coursework**and**oral examination**. - This course is delivered in "intensive mode", i.e. teaching will be concentrated in April and May, students will have June without lectures for working on the coursework, a few lectures will take place in July in preparation for the oral exam.
- As a specialisation of this course, the seminar PT is offered.
- Regular attendance is particularly recommended for this course.

Schedule of Classes in April (slots marked with * in room 2026, otherwise room E005):

Mon | Tue | Wed | Thu | Fri |

5 DS5 | ||||

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):

Mon | Tue | Wed | Thu | Fri |

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 |

21 | 22 | 23 | 24 | 25 |

17/5: public holiday.

*05.04.12—Lecture 1*Introduction 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.12—Lecture 2** *Examples and exercises on axiomatic systems.

*11.04.12—Lecture 3*Natural 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.12—Lecture 4*Natural Deduction: Extension to classical logic. Examples of deductions. Discussion on the rules.

*17.04.12—Lecture 5*Managing 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.12—Lecture 6 and 7*Sequent calculus presentation of natural deduction: systems N_I and N_C. Examples and exercises. Comparison with HBK systems.

*20.04.12—Lecture 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.12—Lecture 11*Equivalence of LK and G_C: translations in both directions.

*25.04.12—Lecture 12 and 13*Cut-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.12—Lecture 14*Semantical Cut-elimination theorem. Applications/consequences of cut-elimination: consistency.

*02.05.12—Lecture 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.12—Lecture 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.12—Lecture 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.12—Lecture 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.12—Lecture 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.12—Lecture 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.12—Lecture 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.12—Lecture 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 @)