You are here:

73094 - Logical Fundaments of Informatics (1) (LM)

Academic Year 2022/2023

                
                        Docente:
                        Claudio Sacerdoti Coen
                    
                        Credits:
                        6
                    
                        SSD:
                        MAT/01
                    
                        Language:
                        Italian
                    
                        Teaching Mode:
                        Traditional lectures
                        
                            Campus:
                            Bologna
                        
                            Corso:
                            Second cycle degree programme (LM) in
                            Philosophical Sciences (cod. 8773)

                                Also valid for
                                
                                    Second cycle degree programme (LM) in
                                    
                                        Computer Science (cod. 5898)
                                    
                            Teaching resources on Virtuale

Course contents

First module:

1. Propositional and First-Order Logic (recall)

Syntax, Semantics, Soundness and Completeness, Undecidability of First Order Logic

2. Untyped Lambda Calculus

Syntax and operational semantics. The lambda-calculus as a programming language: evaluation strategies and encodings of data types; Turing completeness

3. Meta-theory of untyped lambda calculus

Confluence.

4. Simply typed lambda-calculus and Curry-Howard isomorphism

Curry's style and Church's style syntaxes. Isomorphism with propositional minimal logic. Type checking and type inference algorithms.

5. Meta-theory of simply typed lambda-calculus

Weak and strong normalization theorems

6. Curry-Howard isomorphism and extensions to the typing system

Products and coproduts, empty and singleton types. Parametric polymorphisms (minimal introduction to System-F). Minimal introduction to dependent types and Hindley-Milner polymorphisms.

Second module:

1. Logic and Databases

Relational algebra, FO as Query Language, Cilindrical Algebras, Implementation aspects

2. Logic and Computational Complexity

Finite structures and decision problems. NP and PSPACE characterization via first order logics. SAT Solving.

3. Logic and Formal Methods

LTL and CTL: syntax and semantics. Reactive systems and their verifications. Model Checking.

4. Logic and Artifcial Intelligence

Epistemic logic: syntax, semantics, applications

Readings/Bibliography

First module:

- H.P. Barendregt: The Lambda Calculus, Its Syntax and Semantics (Studies in Logic and the Foundations of Mathematics, Volume 103). Available on-line at http://www.cs.unibo.it/~sacerdot/fli1718/barendregt.pdf

- J.Y. Girard, Y. Lafont, P. Taylor: Proof and Types. Available on-line at http://www.paultaylor.eu/stable/Proofs+Types.html

The topics in the first book (by Barendregt) that we will study in the course are also explained in the following notes by the same author:

http://www.cs.unibo.it/~sacerdot/fli1718/IntroductionToLambdaCalculus.pdf

Second module:

- N. Immerman. Descriptive Complexity. Springer, 1999. http://people.cs.umass.edu/~immerman/book/descriptiveComplexity.html

- J. Ullman. Principles of database and knowledge-base systems, Volume I. Computer Science Press, 1990.

- E. Clarke and O. Grumberg and D. Peled. Model Checking. MIT Press, 1999.

Teaching methods

The course is in the first semester. All lessons are frontal lessons, in presence and on-line, unless sanitary requirement force on-line lessons only.

All the topics are presented, with detailed proofs of most theorems.

Depending on the arguments, either slides or the blackboard will be used.

Assessment methods

Oral exam.

Teaching tools

Slides and pointers to scientific articles and books freely downloadable from the Web.

Office hours

See the website of Claudio Sacerdoti Coen