LOGIC
Algebra e Geometria
The exam consists of an interview aimed to verify the acquisition and the correct understanding of the contents of the course. Logical argumentation skills will be checked by asking the detailed proofs of two theorems demonstrated in the course. In addition, knowledge of automatic demonstration methods will be required through simple exercises during the oral test. Examples of oral exam questions are on the e-learning site of the course. The assignment of the final grade will be determined by 50% from the knowledge and understanding of the theorem demonstrations, to 30% from the knowledge of definitions and examples of the concepts dealt with during the course and the remaining 20% from the proper conduct of the exercises.
During the course, written tests could be organized in such a way that, if passed, a reduced oral test will be taken.
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
• 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
Lectures