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.

• Before the next lecture, study the examples of proofs illustrated using the system HT; you may try for other vaild formulae.

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.

• Before the next lecture, try to re-do the deductions already illustrated and/or try with new examples.

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.

• Before the next lecture, re-think to the example shown to justify 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.

• Before the next lecture, try to find proofs for the proposed exercises.

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.

• Before the next lecture, revise the material presented so far.

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.

• Before the next lecture, revise the material presented so far. Also, refer to sections 5 and 6 of Gallier to see how the transformations between proofs in G_I with/without cut to deductions in N_I are defined. Find a proof in G_C for the same formula proven in class in LK.

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.

• Before the next lecture, revise the material presented so far.

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

• Before the next lecture, revise the material presented so far. You may practice the Tait-Girard reduction lemma on cases not seen so far, for example when a cut formula A is active in both subproofs P1,P2 of some logical rule such as implication and existential quantification), or when a cut formula A is passive in a subsequent application on the left subproof of a logical rule, e.g. implication and negation.

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.

• Before the lecture of next week, revise the material presented so far. You may practice the Tait-Girard reduction lemma on cases not seen so far, for the case analysis illustrated today.

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

• Before the next lecture, revise the material presented so far. As an exercise try to see how to transform proofs in one of the G3 system into one of the systems seen so far in the corresponding logic. Prove in G3 tautologies you have already proven in other systems and appreciate the differences in the proof search.
• We will temporarily set aside linear logic, but we will go back to it very soon.

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.

• Before the next lecture, revise the material presented so far. As an exercise, you may formally try to prove that MNPS (with or wiithout the intuitionistic restriction) is equivalent to known systems of the G3 family, or to LK.

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.

• A useful reference for this part is the paper "A Tutorial on Proof Theoretic Foundations of Logic Programming" by Bruscoli and Guglielmi, linked here and slides from an old presentation.

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.

• Most of what has been presented today is available in Gallier's Part 2.

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.

• A useful reference for this part is Lutz Strassburger's course notes on Deep inference and Proof Nets, presented at ESSLLI summer school in 2006. Refer to chapters 1 and 2 (until 2.6 included).

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.

• Use the same reference as above.

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.

• You may refer to Chapter 3 of Lutz Strassburger's course notes on Deep inference and Proof Nets.

07.06.11—Lecture 18 Atomic Flows from SKS derivations.

• The recent talk on 31.5.11 has suscitated the request by some of view to know more about atomic flows (in particular Amin and Ahmed). The purpose of this and the next lecture is to introduce atomic flows on a slightly more technical level than in the talk and compare, in the broad, some of their features with the already seen proof nets (for linear logic). This material will be not part of the exam. You may refer to the following paper by Guglielmi and Gundersen: Normalisation control in deep inference via atomic flows.

08.06.11—Lecture 19 Streamlining of derivations with atomic flows.

• Continuing the previous lecture, this material will be not part of the exam. You may refer to the following paper by Guglielmi and Gundersen: Normalisation control in deep inference via atomic flows.
  

21.06.11—Lecture 20 Gödel first incompleteness theorem.

• Continuing in serving some requests from students (Amin), I will go through a reasonably detailed but not too heavy proof of Gödel's incompleteness theorem, starting from the first one. This material will be not part of the exam.
  

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

• For the presented intermediate logics you may find useful some reading from the Negri and von Plato's book listed among the References. In Vienna, one of the partner university for this study program, there is a very active group working on intermediate logics. This material will be not part of the exam.
  

29.06.11—Lecture 22 General matters arising.

• No material available, sorry, please contact Amin should you need to know more.
  

Material covered and to be prepared for the exam

• In principle, all what has been covered and is listed in Lectures and topics.

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