Degree course: 
Corso di First cycle degree in COMPUTER SCIENCE
Academic year when starting the degree: 
Academic year in which the course will be held: 
Course type: 
Supplementary compulsory subjects
Second semester
Standard lectures hours: 
Detail of lecture’s hours: 
Lesson (32 hours), Exercise (24 hours)

The prerequisites for a profitable learning and for achieving the objectives of the course include the basic mathematical notions and the proof techniques imparted in the fundamental teaching of Algebra and Geometry of the first year, which is therefore a pre-requisite.

Final Examination: 

The exam aims to verify the acquisition and the correct understanding of the contents of the course. The exam is written and structured as follows: (part A) two questions concerning the notions presented in the course and their application; (part B) the proof of a theorem demonstrated in the course; (part C) five exercises of the kind discussed during class exercises.

The final grade will be determined as follows: 30% from the knowledge of definitions and examples of the concepts dealt during the course (part A); 20% from the knowledge and understanding of the theorem demonstrations; 50% from the proper conduct of the exercises.

The final grade is expressed in a score out of 30, where 18 represents the minimum and 30 the maximum.

Voto Finale

This course aims to provide the fundamental knowledge of logical inferences through the study of the basic notions of classical propositional logic and first order logic. Such knowledge is aimed at forming and increasing the ability to manage abstraction of information through symbolic representation and thus the ability to understand an abstract and symbolic scientific language. Some insights into more applicative tools such as SAT-solver and non-classical (modal and fuzzy) logic for program verification will be mentioned. Expected learning outcomes include the ability to identify any error in a mathematical argument and the language skills needed to enunciate a theorem and describe its proof. The logical mechanisms of mathematical reasoning enable the acquisition of adequate skills for improving knowledge and the individual development of new expertise.

Propositional Logic
• What is logic: inferential methods and deduction. The language of propositional logic. Propositional connectives. Semantics of Propositional Logic. Truth tables. Satisfiable formulas and tautologies. (4h)
• Satisfiable sets, logical consequences, deduction theorem. Logical Equivalence, Algebra of Equivalence Classes of formulas, Boolean Algebras. Functional completeness and DNF and CNF. The fundamental equivalences, transformation of a formula into normal form. (6h)
• König's Lemma and Compactness Theorem. (2h)
• Automatic demonstration methods: the Tableaux. Completeness and correctness theorem for tableaux, Hintikka set. (4h)
• Other deductive systems: Sequents. Clauses, resolution, Davis Putnam's procedure, completeness and correctness of the Davis-Putnam procedure. Krom clauses and Horn clauses (6h)

First order logic
• The language of the logic of predicates, terms, and formulas. Range of action of a quantifier, free and bound variables, substitutions. (2h)
• Structures, interpretations and evaluations. Satisfiable and valid forms. Models of a formula. Logical equivalences for logic of predicates. Normal form, Skolem formulas. Transformation of a formula in Skolem form and equisatisfiability. (6h)
• Tableaux for logic of the predicates, theorem of soundness and completeness for the tableaux (4h)
• Herbrand theory: universe and Herbrand base, Herbrand models. Herbrand extensions, Herbrand theorem. (4h)
• Resolution for propositional calculus and logic of predicates, unification algorithm. Completeness theorem for propositional resolution, lemma lifting, completeness theorem for predicates calculation. (6h)
• Horn clauses, logic programming and SLD resolution. Examples of programs. (4h)

Non classical logics
• Kripke structures. Minimum modal logic, examples of modal formulas that characterize properties of Kripke structures, temporal logic. (4h)
• Truth tables of multiple value logic, T-norms and fuzzy sets, logic of continuous t-norms. (4h)

Logica ad Informatica, di Asperti, Ciabattoni.Ed. McGraw-Hill

Slides and exercises (PDF) are available on the e-learning platform.

The teaching activities include lectures (32h) and class exercises (24 ore). The arguments presented during lectures are applied through class exercises; students are expected to actively participate in exercise discussion. The presented exercises have an essential role in preparing the final exam.

Office hours: by appointment via email.