Knowledge and understanding, Learning the basic concepts of computability, complexity and the elementary notions about propositional logic and predicate logic. Applying knowledge and understanding. Acquire the ability to formally define problems using the language of logic or to formally specify a problem or the behavior of a system by exploiting one of the studied computational models. Making Judgement. Understanding the intrinsic limits of computability or the intrinsic complexity of problems to reason about the effectiveness and feasibilty of designing algorithmic solutions to a problem. Communication skill. Ability to rigorously and formally define and communicate concepts and problems. Learning skills. Ability to independently read the literature proposing formal methods for symbolic artificial intelligence (and knowledge representation) and computer science in general.

The basics of set theory. Understanding the basic formal notation of mathematics.

The course consists of three main parts each quantifiable in 3 CFU: - Computability. The main computational models will be examined by reasoning on their expressiveness. In particular, in increasing order of expressiveness we will first introduce regular automata, then pushdown automata and context-free grammars. To define the notion of computability we will finally study Turing machines and the notion of decidability. We will study the expressiveness relationships between the computational models, their properties with respect to the operations of composition and we will prove that there are problems for which there are no algorithmic solutions (undecidable problems). - Complexity. The basic notions of spatial and temporal complexity will be illustrated. In particular, the best known complexity classes will be studied: P, NP, NP-Complete, coNP, EXP and PSPACE. For each class we shall consider representative problems belonging to the class. Particular attention will be paid to the class NP-Complete by introducing the notion of complete problem and the reduction technique (useful for determining the complexity of a problem). Such a reduction technique will be exemplified in some significant cases (e.g. SAT, 3SAT, Hamiltonian Path, k-Clique, etc. ). - Logic. Syntax and semantics of propositional logic and (first order) predicate logic will be introduced. We will study the satisfiability problems for both logics. The techniques of tableaux, resolution and refutation will be introduced. We shall study the best known algorithms for SAT for propositinal Logic. We will study suitable normal forms for predicate logic (prenex form, clause form) and Goedel's theorem for the refutation of predicate logic in clause form. We shall consider Logic Programming with a breaf introduction to the Prolog language. Finally we briefly introduce the specification environment Z3.

For the part of calculability and complexity: [1] Michael Sipser, Introduzione alla teoria della computazione, Apogeo. For the part of Logics: [2] Mordechai Ben-Ari: Mathematical Logic for Computer Science (3rd ed.), Springer, 2013. (for a reference in italian see also) [3] Daniele Mundici, Logica-Metodo breve, Springer, 2011.

- Basic notions: Alphabets, words and languages - - The regular automata - Deterministic and non-deterministic automata: syntax and semantics. - Determination of regular automata - Regular languages ​​and their closure by union, intersection, complement, concatenation and *. - Regular expressions: syntax and semantics - Equiexpressiveness of regular automata and regular expressions - Pumping lemma for regular languages - Use of the Pumping lemma to prove the non-regularity of languages - Pushdown automata (non-deterministic): syntax and semantics - Context free languages - Context free grammars for generating context free languages - Pumping lemma for context free languages - Non-closure by intersection and complement of pushdown automata - Turing machines (deterministic and non-deterministic): syntax and semantics. - Languages ​​recognized and decided by MdT - Equivalence of multitape MdT - Determinization of the MdT - Characterization of decidable languages - Countability of Turing machines and uncountability of languages - Examples of undecidable languages. - Spatial and temporal complexity for languages - Class P and problems decidable in polynomial time by deterministic MdT - Class NP and problems decidable in polynomial time by non-deterministic MdT - Polinomial time reduction among problems - Class NP-Complete - Cook-Levin Theorem (NP-completeness of SAT) - Other NP-complete problems: 3SAT, k-Clique, Hamiltonian path. - The coNP class and examples of coNP-complete problems - Spatial complexity classes: PSPACE and NPSPACE - Savitch's theorem (PSPACE = NPSPACE) - PSPACE-complete problems: quantified boolean logic. - Logic - Propositional calculus: syntax and semantics. - Logical implication, equivalence, tautologies, satisfability. - Semantic tableaux - Conjunctive and disjunctive normal form. - Davis-Putnam algorithm - Correctness and completeness of the Davis-Putnam algorithm. - Other algorithms for SAT solving - Refutation - Krom clauses and Horn clauses - Calculus of predicates: syntax and semantics - Semantic Tableaux - Prenex normal form - Skolemization - Reduction in clause form - Herbrand universe - Goedel's theorem for refutation - Unification algorithm - Logic programming and SDL resolution - Introduction to Prolog - SAT in Z3

In-class lectures and exercises. Homework assignements and in-class correction of exercises.

Slides, exercises, previous exams can be found in the shared folder in the team channel fr the course.

The exam consists of a written test and a subsequent oral test. The written test involves solving exercises on the part of Computability and that of Logic, as well as general questions on the topic of complexity. The written test comprises 6 open-answer exercises. Each exercise is assigned a score, and the total amount of points assigned to the exercises is 32. The maximum score for an exercise is given for a correct solution of the exercise. In the presence of errors, the maximum score is reduced according to their severity. The score for the written test is equal to the sum of the scores obtained in the individual exercises. The student is allowed to take the oral exam if they have obtained at least a minimum score of 18 in the written test. The written exam can optionally be taken in two parts: 1) Computability and complexity; 2) Logic. In this case, the scores from the two parts will be averaged. The oral exam is primarily (but not exclusively) focused on the part of complexity and logics. The questions focus on the definition of basic concepts, the proofs of the theorems presented in the course, and the reasoned understanding of the general concepts. The degree of knowledge, the precision of the exposition, and the ability to articulate autonomous reasoning will be evaluated. The oral exam is scored out of thirty (independent of the score achieved in the written exam). The final grade averages the score obtained in the written exam with the evaluation reported in the oral exam (which must be at least 18/30). The distinction of honors is awarded to those who achieve the maximum score in both the written and oral exams. The oral exam may alternatively be replaced with the development of a project in the specification environment Z3 to be agreed upon with the teacher.

This course explores topics closely related to one or more goals of the United Nations 2030 Agenda for Sustainable Development (SDGs)