The teaching is organized as follows:

Learning outcomes

Module: BASI DI DATI
-------
-


Module: LOGICA COMPUTAZIONALE
-------
The main theme of this module is logic computation as "proof-search/search for a counterexample" for classic, intuitionistic, modal and temporal logics: for any one of such logic, given a formula A find a proof of A or a model falsifying A. The preferred method, when possible, are Gentzen-systems, in particular the sequent calculus, as it yields not only an elegant proof system (top-down derivation) - which has a non-trivial relation with Natural Deduction systems - but also a procedure for constructing counterexamples ("semantic tableaux" procedure, bottom-up search).

After a recapitulation of the completeness theorem for the classical propositional and first-order sequent calculus with respect to Tarski's semantics, the procedure is extended to various modal systems (K, KD, K4, S4), yielding the completeness theorem and the finite modal property for Kripske's semantics.

An extension of Gentzen's methods to temporal logics PLTL and CTL is still theme of ongoing research; after a presentation of the linear time and branching time semantics, materials are given for further study on the topic.

The issue of the relations between intuitionistic natural deduction NJ and the sequent calculus LJ is dealt by showing the correspondence between cut-free LJ derivations and normal NJ deductions, also with an introduction to the theorem on the permutation of inferences; moreover the algorithms for cut-elimination in LJ and weak normalization of proofs in NJ are studied and examples are given of confluence and non-confluence in classical, intuitionistic and linear logics.


Module: LINGUAGGI
-------
The aim of the course is to present the theoretical basis of programming languages.A number of paradigmatic higher order typed languages will be introduced (lambda calculi). The entire course will focus on the concepts of type systems and of operational semantics. The problem of definition of data types will be analyzed.

Program

Module: BASI DI DATI
-------
-


Module: LOGICA COMPUTAZIONALE
-------
PART 1 - (a) Semantic Tableaux for classic and modal propositional logic.
Classical logic as logic of truth. Semantic tableaux for classical propositional logic; completeness theorem. Kripke' semantics pf propositional modal logics K, KD K4, S4. Temporal logic, linear and branching time: basic semantic notions.

(b) First ordet predicate calculus.
Recalls of classical semantics. Semantic tableaux procedure and completeness theorem for first order predicate calculus.

PART 2 - Sequent Calculus.
Basic notions, subformula property, cut rule. Permutation of inferences. Cut-Elimination and proof-normalization. Strong and weak normalization. Examples. Basic notions of linear logic and proof-nets.

PART 3 - Intuitionistic Logic.
Intuitionistic logic as logic of assertability and Heyting and Kolmogorov's interpretation. Intuitionistic natural deduction (implicative fragment with products). Curry-Howard correspondence (basic notions). Correspondence between Natural Deduction and Sequent Calculus. Modal interpretations of intuitionistic logic (basic notions).


Module: LINGUAGGI
-------
Inductive definitions; transition systems; type systems; structural operational semantics. Higher order languages and calculi: typed lambda calculus and Curry-Howard isomorphism;system T: syntax, semantics, definability and data types; PCF: syntax, semantics, definability and data types; system F: syntax, semantics, definability and data types.

Bibliography

Examination Methods

Module: BASI DI DATI
-------
-


Module: LOGICA COMPUTAZIONALE
-------
Written test.


Module: LINGUAGGI
-------
The exam consists of a written test.