Computational Logic
Verona - Autunn 2008
- PART 1 (Until November 17)
- Basic Proof-theory of intuitionistic and classical logic.
Monday 6th October: Forms of common sense reasoning and proof-theory.
Wednesday 8th October: Intutionistic Natural Deduction NJ for
implication and conjunction.
Monday 3rd November: Weak Normalization Theorem for Natural Deduction
NJ. Reduction strategies.
Wednesday 10th November: Intuitionistic Sequent Calculus LJ
without cut. Subformula Property. Correspondence between normal
NJ derivations and cut-free LJ derivations.
Wednesday 12th November: Introduction to the Classical sequent calculus
and semantic tableaux procedure for LK
- Elements of lambda calculus.
Monday 13th October: Introduction to the Lambda Calculus and to
the Curry-Howard correspondence: decoration of NJ derivations with
lambda terms.
Wednesday 15th October: Review of Computability Theory: primitive
recursive and partial recursive functions.
Wednesday 5th November: Formal treatment of the lambda calculus:
notions of substitution, alpha-equivalence, weak and strong normalization.
Wednesday 12th November: Proof of the Church Rosser property for
the untyped lambda calculus.
-
Midterm November 17th
- PART 2
- Elements of Categorical Semantics (Dr Kurt Ranalter):
Wednesday 19th November: Definition of a Category;
Cartesian Categories; Exemples and Exercises.
Monday 24th November: Cartesian Closed categories.
Wednesday 26th November: Categorical Soundness and Completeness
(outline).
- Special Topics. Modal Logic.
Wednesday 3rd December: Modal Logics K, K4, S4.
Sequent calculi, Kripke semantics and semantic tableaux procedure.
- Special Topics. Modal Logic.
Wednesday 10th December: Introduction to Classical and Intuitionistic
Linear Logic.
- Written exam on part 2:
preexam December 17th
solutions here!
- SEMINARS.
- Proof-theory, lambda calculus and category theory.
Wednesday 10th December, 16:30: Alessandro Caldana, Marco Carazzolo and
Nikolic Djuricza: Cpo's with continuous maps form a CCC.
Monday 15th December, 09:30: Cut elimination for the classical
sequent calculus LK
Wednesday 17th December, 16:30: Denis Mantovani, Dario Meloni,
Davide Benetti and Federica Panarotto: Cut elimination and term assignment
for LJ and Intuitionistic Multiplicative Linear IMLL sequent calculus.
Stefano Soffia: Implication is right adjoint of conjunction.
Thursday 18th December 18:00 Simone Campedelli, Andrea Brazzarola, Simone Ferrarini
and Erisa Karafili:
On Robin Gandy's proof of strong normalization for the simply typed
lambda-I calculus.
Monday 22nd December 18:00 Vladan Mijatovic, Daniele Corso and Nicholas Pavan:
Proof-theory of the modal systems IK (intuitionistic) and CK (classic).
Tuesday 23rd December 18:00 Michele Peroli, Mattia Tommasi e Davide Guardini
Categorical semantics of IK and of IMLL .
- EXAM DAY (Winter session): Wednesday 7th January 2009:
- Regular Exam 10:00-12:30
- Seminar Reports (afternoon): Each group presents the main results
of their investigations (10 minutes for each person in the group).
The presentations give an overview of the topics of the course
(proof-theory, lambda calculus and categorical semantics).
- Cut elimination and term assignment for LJ and IMLL;
- Natural Deduction for IK and CK;
- Categorical Semantics for IK and IMLL;
- Strong Normalization Theorem.
- EVALUATION Two forms of exam:
- End-of-term Evaluation: Written exam, during regular exam sessions.
- In-term Evaluation:
- Coursework 30 percent
(average of 5 best marks among at least 7 assignments)
- Midterm 30 percent on Part 1 (November 17, 9:30-11:30)
- Final Exam 40 percent (December 17, 11:30-13:30)
- Possibly replaced by
- a seminar (to be agreed with the instructor) and oral exam.
Lecture notes:
-
Synsem.pdf,
Girard, J.-Y. : Linear Logic, its syntax and semantics, Advances
in Linear Logic, eds Girard, Lafont, Regnier, London Mathematical Society
Lecture Notes Series 222, Cambridge University Press 1995.
- Natural Deduction:
Weak Normalization Theorem for NJ (Lecture Notes pp.20-1);
reduction of all applications of the intuitionistic (`bottom-int') and classic
(`bottom-C') falsity rules to inferences with atomic conclusions only.
- Lambda calculus:
Church Rosser Property.
- Exercise: 1: pdf
Assigned: October 8th -- due: October 13th 2008
- Exercise 2: pdf Assigned: October 20th
Solution Exercise 2: pdf
- Exercise 3: pdf Assigned: October 20th
Solution Exercise 3: pdf
- Exercise 4: pdf
Assigned: October 27th
Solution Exercise 4: pdf
There has been a misunderstanding in the marking of Coursework 4:
Dr Ranalter has evaluated the papers according to a common definition
of capture-avoiding substitution, rather than the one given in class,
resulting in a lower grade for some people than they deserve.
To see whether you may receive one more point for your work,
do the following:
- Download the revised version of Krivine's book at
http://www.pps.jussieu.fr/~krivine/;
- read Section 2 on Alpha conversion, in particular pages 15-16;
- understand why the definition at page 16 used by Dr Ranalter is
equivalent to that given in class;
- come to my office, explain this equivalence to me and
have your mark upgraded.
- Exercise 5: pdf
Assigned: November 5th -- due: Wednesday November 12th 2008.
- Exercise 7: pdf
Solutions to Part 1. pdf
- A seminar is a (sequence of) meetings in which a particular topic
is studied through presentations and discussion.
To be active part
of a seminar one has to give a presentation on a commonly agreed topic
and attend all the meetings (reasonable excuses are accepted).
- Partecipation in a seminar and final colloquium are worth 40
per cent of the final mark.
- This option is therefore equivalent with and can substitute the final
written exam,
if the midterm has been passed.
- Alternatively partecipation in a seminar can substitute the midterm, if
this has not been successful, but the final written exam is required.
- You have at least a week for preparing a seminar presentatio,
after agreeing the topic and bibliography with an instuctor.
Proof theory
- (1)-(4) Give term assignments to the sequent calculi
and prove the cut elimination theorem for the following
- the sequent calculus LJ with implication and conjunction.
- the sequent calculus IMLL for intuitionistic multiplicative
linear logic with linear implication and tensor.
- (5)-(6) Prove the normalization theorem for a natural deduction
system for the modal logics K and
K4
- Further topics on Proof Nets for MLL (multiplicative classical
linear logic and variants) can be arranged.
Categorical Semantics
- (1)-(5) Choose one of the three tasks in
pdf.
The first two tasks on modal and linear logic correspond each to two seminar
presentations (one, prove soundness and, two, completeness of the semantics).
- (6) Show that Heyting algebras with g.l.b.
(greatest lower bound)provide a canonical algebraic interpretation
and a degenerate categorical interpretation of minimal logic NJ
with implication and conjunction.
Bibliography: Lecture Notes Chapter 5 ps pp. 63-89.
- (7) Show that
cpo (complete partial ordering)
with continuous maps form a CCC.
Bibliography: A. Pitts. Lecture Notes on Denotational Semantics
(Part II CS Tripos, Univ. Cambridge)
pdf,
pp.1-28
Lecture notes ps Chapter 6, pp.124-136.
Lambda calculus
- (1) Dimostra che le funzioni parziali ricorsive sono
lambda-I definibili.
Bibliografia: Dispense (Federico Aschieri)
pdf, pp.1-3
H.P.Barendregt: The Lambda Calculus Its Syntax and Semantics pp.185-214.
- (2) Dimostra che l'insieme dei lambda termini normalizzabili
non e` ricorsivo.
Bibliografia: Dispense (Federico Aschieri)
pdf, pp.4-5
- (3) Completala prova semantica del
Teorema di normalizzazione forte per il lambda-I calcolo (R.Gandy),
nella versione presentata in classe da Federico Aschieri.
Bibliografia: Dispense (Federico Aschieri)
pdf, p.5.