Logica Computazionale

Verona - 7 ottobre - 12 novembre 2009



Bibliografia:

  • Stirling, Colin. Models and calculi for concurrent computation, modal and temporal logics. In Handbook of Modal Logic editors P. Blackburn, J. van Benthem and F. Wolter.

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

    Coursework:
  • Compito per casa 1: pdf Assegnato: 8 ottobre 2009 -- da consegnare: 15 ottobre.
    Soluzione Compito per casa 1: PDF oppure Lovato 1.
    • Si noti che in Es 1(e) tutti i sequenti hanno al massimo una formula nel succedente.
    • In Es 2(b) un controesempio alla invertibilità semantica del Cut moltiplicativo è dato da
      Γ1 = bottom , Γ2 = top ∆1 = A , ∆2 = bottom,
      dove bottom è una costante proposizionale contraddittoria e top una costante proposizionale valida.

  • Compito per casa 2: pdf Assegnato: 22 ottobre 2009 -- da consegnare: 29 ottobre.
    Soluzione Compito per casa 2: Lovato 2.
  • Si noti che in Es 2 nell'applicazione della procedura è stato omesso il termine iniziale a nel sequente-conclusione. Questo non ha conseguenze in questo caso: un tale termine non comparirebbe nella formula atomica L(a1,a0) che consente di chiudere il ramo considerato.
  • Compito per casa 3: pdf Assegnato: 2 novembre 2009 -- da consegnare: 9 novembre.
    Soluzione Compito per casa 3: Lovato 3.
  • Compito per casa 4: pdf Assignato: 12 novembre 2009 -- da consegnare: 19 novembre.
    Soluzione Compito per casa 4: Lovato 4.
  • Complementi su deduzione naturale, calcolo dei sequenti, normalizzazione, eliminazione del cut pdf