Foundations of Computing - LOGICA COMPUTAZIONALE (2009/2010)

Course code
4S02789
Name of lecturer
Gianluigi Bellin
Number of ECTS credits allocated
4
Other available courses
Academic sector
INF/01 - INFORMATICS
Language of instruction
Italian
Location
VERONA
Period
1st Semester dal Oct 1, 2009 al Jan 31, 2010.

To show the organization of the course that includes this module, follow this link * Course organization

Lesson timetable

1st Semester
Day Time Type Place Note
Tuesday 2:30 PM - 4:30 PM lesson Lecture Hall I from Oct 1, 2009  to Nov 21, 2009
Wednesday 10:30 AM - 12:30 PM lesson Lecture Hall I from Oct 1, 2009  to Nov 21, 2009
Thursday 2:30 PM - 4:30 PM lesson Lecture Hall I from Oct 1, 2009  to Nov 21, 2009

Learning outcomes

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.

Syllabus

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

Assessment methods and criteria

Written test.