Computational Logic

Verona - Autunn 2008


Lecture notes:

    Coursework:
  • 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 6: pdf
  • Exercise 7: pdf
    Solutions to Part 1. pdf

    Seminars. Projects 2008:

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