LOGIC

Degree course: 
Corso di First cycle degree in COMPUTER SCIENCE
Academic year when starting the degree: 
2020/2021
Year: 
2
Academic year in which the course will be held: 
2021/2022
Course type: 
Supplementary compulsory subjects
Seat of the course: 
Varese - Università degli Studi dell'Insubria
Credits: 
6
Period: 
Second semester
Standard lectures hours: 
48
Requirements: 

For a proficient learning of this course, the student has to master the mathematical notions and the proving techniques taught in the fundamental course in Algebra and Geometry during the first year, which is, in a any case, compulsory to pass before taking this examination.

In particular the following notions and techniques are essentials:

- Basis of discrete mathematics: theorems, and proof methods: implications, counter-nominal, reductio at absurdum, proof by induction, combinations and combinations with repetitions, factorial function, binomial coefficient

- Set theory: set, membership and inclusion, subset, power set, cardinality, set operations (union, intersection and complement), pairs and cartesian product, counting the elements of a finite set.

- Relations: relations, properties (reflexivity, symmetry, transitivity), equivalence relations, equivalence class, quotient set, partitions, order relations, least and greatest element, least and upper bounds.

- Functions: domain and codomain, range and preimage, injective, surjective and bijective functions, inverse of bijective functions, function composition.

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.

Assessment: 
Voto Finale

Knowledge and understanding skills
The course aims to provide basic knowledge of logical inferences, through the study of the basic notions of classical propositional logic and of first order logic. Such knowledge is aimed at forming and increasing the abstraction of information through symbolic representation and thus the ability to understand an abstract and symbolic scientific language.

Knowledge and understanding skills applied
Some insights into more applicative tools such as SAT-solver and non-classical (modal and fuzzy) logic for program verification will be mentioned.

Autonomy of judgment and communication skills
Expected learning outcomes include the ability to identify any errors in a mathematical argument, and to have a language property that can enunciate a theorem and describe its demonstration.

Ability to learn
Logical mechanisms of mathematical reasoning enable the acquisition of adequate skills for improving our own knowledge and the individual development of new skills.

Propositional Logic (goals 1-4)
• 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 (4h)

Logic of Predicates (goals 1-4)
• 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 (2h)
• 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. (2h)

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

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 (4h)

Logic of Predicates
• 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 (2h)
• 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. (2h)

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

Slides of lectures, available on the elearning web page of the course

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

The teaching activities alternates the presentations of notions and theorems and their application to the solution of exercises; students are expected to actively participate in exercises discussion. The presented exercises have an essential role in preparing the final exam.

The teacher receives by appointment, upon request by e-mail to mauro.ferrari@uninsubria.it

Professors

Parent course