Structural Proof Theory and Abstract Logic Programming (summer semester 2012)


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.

Material covered and to be prepared for the exam

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.

3Course Info

Lectures and topics

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

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

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

25.04.12—Lecture 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.12—Lecture 14Semantical 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.

4Tutors and Office Hours

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