Structural Proof Theory and Abstract Logic Programming

1References

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

Paola Bruscoli and Alessio Guglielmi
A Tutorial on Proof Theoretic Foundations of Logic Programming

pdf available, and slides from an old presentation

Lutz Strassburger
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
pdf

Xichuan or Amin might have pdf of previous slides, please contact them.

2News

11/5/11 DIES ACADEMICUS (No lectures at TUD)

11-17/6/11 Lecture-free period at TUD (Reminder)

3Course Info

Lectures and topics

05.04.11—Lecture 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.11—Lecture 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.11—Lecture 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.11—Lecture 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.11—Lecture 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.11—Lecture 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.11—Lecture 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.11—Lecture 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.11—Lecture 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.11—Lecture 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.11—Lecture 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.11—Lecture 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.11—Lecture 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.11—Lecture 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.11—Lecture 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.11—Lecture 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.11—Lecture 17 Other fragments of linear logic: MELL, MALL, Cyclic Linear logic, IMLL.

07.06.11—Lecture 18 Atomic Flows from SKS derivations.

08.06.11—Lecture 19 Streamlining of derivations with atomic flows.

21.06.11—Lecture 20 Gödel first incompleteness theorem.

28.06.11—Lecture 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.11—Lecture 22 General matters arising.

Material covered and to be prepared for the exam

Courseworks

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.

4Tutors and Office Hours

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