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
Paola Bruscoli and Alessio Guglielmi
A Tutorial on Proof Theoretic Foundations of Logic Programming
pdf available, and slides from an old presentation
Proof nets and the identity of proofs
(ESSLLI 2006 course notes)
pdf available from the author
Alessio Guglielmi, Tom Gundersen
Normalisation control in deep inference via atomic flows
LMCS Vol 4 (1:9) 2008 pp 1--36
Xichuan or Amin might have pdf of previous slides, please contact them.
11/5/11 DIES ACADEMICUS (No lectures at TUD)
11-17/6/11 Lecture-free period at TUD (Reminder)
05.04.11Lecture 1Introduction to the course, motivations, references. Notions of formal system, axiomatic proof system, Hilbert-Tarski systems for propositional and first order classical logic.
06.04.11Lecture 2More examples of proofs in axiomatic systems. Natural Deduction in Intuitionistic Logic, following Heyting-Brouwer-Kolmogorov: direct proof principle and introduction rules, inversion principle and elimination rules, open and closed assumptions. Example of deductions in the system. Extension to Classical Logic.
11.04.11Lecture 3Some peculiarities of Natural Deduction as presented in HBK calculus illustrated through examples about the management of the assumptions (active assumptions, vacuous discharge, unique discharge, multiple discharge of assumptions). The elimination rule for disjunction. Discussion on adequacy of the representation. Towards the sequent calculus presentation of Natural Deduction.
12.04.11Lecture 4Sequent calculus presentation of Natural Deduction for Intuitionistic and Classical Logic: System N_I and N_C . Basic terminology, notion of sequent in these calculi, examples of derivations and proofs in the given systems.
13.04.11Lecture 5More examples and exercises of derivations in N_I and N_C. Moving towards the sequent calculus systems G_I, G_C and LK. Basic terminology, notion of sequent in these calculi. Structural and logical rules. Comparing some "symmetries" in the calculi along the And-Or Left-Right axes, and the shape of axioms and structural rules.
18.04.11Lecture 6System G_I with and without cut: the role of contraction in the intuitionistic system. Are the two systems equivalent (Does cut-elimination hold)? Reasons to study G_I with and without cut: their relations to N_I and transformations to deductions in normal forms. G_C and LK: justifying their structural rules. Example of proof in LK in first order.
26.04.11Lecture 7Trasformations of proofs from G_C to LK and from LK to G_C. Preliminary definitions for the cut elimination theorem in LK: degree of a formula and cut-rank.
27.04.11Lecture 8Preliminary definitions for the cut elimination theorem in LK: depth and logical depth of a proof. The problem of infinite reductions with cut/contraction and the multicut rule. Proof of Tait-Girard reduction lemma (to be cont'd).
3.05.11Lecture 9(Two lectures on this day: first lecture) Proof of Tait-Girard reduction lemma (completed). Considerations on the bounds in the statement of the Tait-Girard's Lemma. Cut elimination theorem. Semantical proofs of cut-elimination.
3.05.11Lecture 10(Two lectures on this day: second lecture) Consequences and applications of cut elimination: interpolation, Beth's definability theorem, consistency of a proof system. Proof systems of the G3 kind: cut-free and with contraction built-in in sequents: Considerations in system design from the point of view of automated deduction and theorem proving. Systems G3m, G3i, G3c for minimal, intuitionistic and classical logic, respectively. Controlling structural rules: introduction to Linear Logic (connectives, rules, equalities, and intuitive meaning of the connectives).
4.05.11Lecture 11An informal introduction to Abstract Logic Programming: motivations, the rule of "backtracking" in LK. Proof search in terms of application of backtracking macro-rule. Infinite, successful, failing computation in the machine model see in proof theoretical terms. System MNPS (and comparisons with the G3 family, in terms of design). Stated and not proved: its equivalence wih LK. Its restriction to intuitionistic logic. Notions of I-Proof and uniform proof.
10.05.11Lecture 12 (Two lectures on this day: first lecture) Examples of formulae that are provable but not uniformly provable. Restricting the language to gain correspondence between provability and uniform provability: abstract logic programming language. Examples of A.L.P.L: Horn clauses, Harrop's Hereditary Formulae, Higher order, and their uses.
10.05.11Lecture 13 (Two lectures on this day: second lecture) Abstract Logic Programming in Linear Logic: System Forum. Languages LO, Lolli, Lambda-Prolog, and considerations from the point of view of language design (Abstract data type, synchronisation, Abstraction). The problem of sequentialisation as operator in linear logic (causality through linear implication). Removing the inherent sequentiality in sequent's proofs: Proof Nets for Linear Logic. Trying to reconstruct from a Proof Net the Sequential Proof: Deduction Nets, Sequential Deduction, Danos-Regnier criterion of correctness.
24.05.11Lecture 14 Introducing Deep Inference (for a fragment of linear logic). System MLL- (multiplicative linear logic without units) in deep inference and sequent calculus; motivations for the problem of identity of proofs. A pathway from deep inference to proof nets (for MLL-): 1) From sequent calculus to proof nets via coherence graphs and from deep inference to proof nets via flow graphs: cut-free proofs and proofs with cuts; Correctness criterion.
25.05.11Lecture 15 A pathway from deep inference to proof nets (for MLL-): 2) Two sided sequent calculus, two sided proof nets and how to port this to deep inference introducing polarities and using the deep inference top-down symmetries. Discussion on the relevance of the problem of identity of proofs.
31.05.11Lecture 16 Talk by Alessio Guglielmi at 13:15 "Redesigning Logical Syntax with a Bit of Topology". The lecture slot will be used for further discussions.
01.06.11Lecture 17 Other fragments of linear logic: MELL, MALL, Cyclic Linear logic, IMLL.
07.06.11Lecture 18 Atomic Flows from SKS derivations.
08.06.11Lecture 19 Streamlining of derivations with atomic flows.
21.06.11Lecture 20 Gödel first incompleteness theorem.
28.06.11Lecture 21 Gödel second incompleteness theorem. Introduction to some intermediate logics presented in the sequent calculus as extensions of systems G3ip (G3 style, intuitionistic, propositional): invertibility of rules, studying admissibility of rules. Extensions with excluded middle, weak excluded middle (atomic and general forms).
29.06.11Lecture 22 General matters arising.
Here you may find a list of exercises to be submitted by 20/7/2011: use the white postbox out of room 2001.
Their assessment will contribute to the final grade of your exam.
This is meant to be individual work; read carefully the General Notes and don't forget to sign the declaration.
I don't have tutors. The Open House is a good venue for discussing your questions, otherwise drop me an email and we'll arrange for an appointment.
29.6.11Paola Bruscoliemail (replace AT by @)