LOGIC

Degree course: 
Corso di First cycle degree in COMPUTER SCIENCE
Academic year when starting the degree: 
2021/2022
Year: 
2
Academic year in which the course will be held: 
2022/2023
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 open book, lasts 110 minutes, and consists of a number of exercises of the kind discussed during class (e.g. translation from natural language to one of the logics considered, construction of counterexamples, proofs of satisfiability/soundness with one of the techniques used).

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.

Syllogistic Logic
• What is logic: inferential methods and deduction. Historical background. The language of Syllogistic Logic. The Square of Oppositions. Direct and Indirect Proofs, soundness and completeness.

Propositional Logic

• The language of propositional logic. Propositional connectives. Semantics of Propositional Logic. Truth tables. Satisfiable formulas and tautologies.
• 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. (
• König's Lemma and Compactness Theorem.
• Automatic demonstration methods: the Tableaux. Completeness and correctness theorem for tableaux, Hintikka set.
• Other deductive systems: Sequents. Clauses, resolution, Davis Putnam's procedure, completeness and correctness of the Davis-Putnam procedure. Krom clauses and Horn clauses

Logic of Predicates
• The language of the logic of predicates, terms, and formulas. Range of action of a quantifier, free and bound variables, substitutions.
• Structures, interpretations and evaluations. Satisfiable and valid forms. Models of a formula. Logical equivalences for logic of predicates.

Syllogistic Logic
• What is logic: inferential methods and deduction. Historical background. The language of Syllogistic Logic. The Square of Oppositions. Direct and Indirect Proofs, soundness and completeness.

Propositional Logic

• The language of propositional logic. Propositional connectives. Semantics of Propositional Logic. Truth tables. Satisfiable formulas and tautologies.
• 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. (
• König's Lemma and Compactness Theorem.
• Automatic demonstration methods: the Tableaux. Completeness and correctness theorem for tableaux, Hintikka set.
• Other deductive systems: Sequents. Clauses, resolution, Davis Putnam's procedure, completeness and correctness of the Davis-Putnam procedure. Krom clauses and Horn clauses

Logic of Predicates
• The language of the logic of predicates, terms, and formulas. Range of action of a quantifier, free and bound variables, substitutions.
• Structures, interpretations and evaluations. Satisfiable and valid forms. Models of a formula. Logical equivalences for logic of predicates.

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 pietro.galliani@uninsubria.it

Professors

Parent course