Risorse bibliografiche
Risorsa bibliografica obbligatoria
Risorsa bibliografica facoltativa
Scheda Riassuntiva
Anno Accademico 2019/2020
Scuola Scuola di Ingegneria Industriale e dell'Informazione
Cfu 5.00 Tipo insegnamento Monodisciplinare
Docente Mauri Luca

Corso di Studi Codice Piano di Studio preventivamente approvato Da (compreso) A (escluso) Insegnamento

Obiettivi dell'insegnamento

This is an introductory course in logic, focusing on the basic techniques and theorems of first order logic and on some of their applications. It is also meant to provide sound foundations for the use of formal languages both in mathematics and computer science and to lay the ground for more advanced courses in logic. Along the way, algebraic concepts will be introduce as instrumental to the development of Tarski's semantics of first order logic and in order to provide interesting models of theories. Lab sessions will be used to present a theorem prover and to discuss its use in the automation of proofs. By the end of the course the student should be able to formalize simple reasonings from mathematics and natural language using first order languages and to check their correctness in classical first order logic, both manually and with the help of software.

Risultati di apprendimento attesi


Dublin descriptor

Expected learning outcomes

Knowledge and understanding

  • Understand the structure of a logic, syntax, semantics and calculi using propositional and first order logic as paradigms; understand how these components tie together to provide tools that can be used to analyse problems in mathematics and computer science. Know how to work with first order languages and how to derive conclusions from premises using both semantical tools and calculi, in particular the Hilbert calculus and resolution.
  • Understand some of the basic concepts in the foundations of mathematics, relations and functions in particular and how these concepts are used in the construction of mathematical structures and how they are abstracted into first order languages. Know how to work with basic algebraic structures like groups, rings, lattices.
  • Understand the interplay between logic and algebra, how algebraic structures and relations generalize into languages and conversely how the logical tools can be used to prove properties of algebraic structures.

Applying knowledge and understanding

  • The final result of the course should be the ability to take a problem suitable for mathematical formalization, select a formal language to describe the relevant properties of the problem and then use the logical tools to examine the problem, either by producing counterexamples to simple conjectures or to prove others using the calculi.
  • The student is also expected to apply the knowledge gained in the course to use automated theorem provers at least in some simple cases.

Learning skills

  • Develop habits and tools for abstract thinking.
  • Lay the foundations for more advanced courses in logic and mathematics
  • Learn to use abstract mathematical tools to model concrete problems.

Argomenti trattati
  1. Propositional logic. Syntax: the language of propositional logic, variables, connectives, formulas. Semantics: evaluations, truth tables, models, satisfiability. Semantic equivalence. Normal forms. Calculi: deductive systems, axioms, theorems. The Hilbert calculus system for PL. Soundness and completeness. The resolution calculus for PL.
  2. Relations and functions. Relations, operations with relations, representation by graphs and incidence matrices, closure operators. Equivalence relations and quotient sets. Order relations, posets, lattices. Functions, invertibility of functions, isomorphism theorems and factorizations. Cardinalities: definition, characterization of infinite sets, Cantor's theorem. Operations.
  3. First order logic. Syntax: variables, function and predicate symbols, terms, atomic formulas, formulas, languages. Free and bound variables. Semantics: interpretations, models, satisfiability, validity. Prenex form. Skolemization. The resolution calculus for first order logic: substitution, unification. Soundness and completeness. The Hilbert system for first order logic. First order theories: theories, theories with equality, algebraic theories, models.
  4. Algebraic structures. Internal operations, neutral elements, associativity, commutativity. Algebraic structures: semigroups, monoids, groups, abelian groups, rings, fields, skew fields. Morphisms of structures. Substructures. Congruence relations on a structure and quotients. Modular arithmetic. Morphisms of structures and their factorization. Normal subgrups and ideals. Boolean algebras.



There is no logic prerequisite for this course. Nevertheless, knowledge of linear algebra from geometry courses and of elementary set theory from calculus courses is strongly recommended as it will be needed when working with examples of algebraic structures.

Modalità di valutazione

Students will have to take a written exam to earn a pass grade; the exam may comprise both exercises and theoretical questions. There will also be an opportunity, for students regularly attending the course, to write classworks for each section of the course which, when fully completed as indicated by the lecturer, will contribute significantly toward the final grade.

Risorsa bibliografica obbligatoriaA. Cherubini. Lecture notes https://beep.metid.polimi.it

Available from the course page on the Beep platform

Risorsa bibliografica obbligatoriaExercises beep.metid.polimi.it

Available from the course page on the Beep platform

Risorsa bibliografica facoltativaM. Fitting, First order logic and automated theorem proving
Risorsa bibliografica facoltativaS. Hedman, A first course in logic
Risorsa bibliografica facoltativaE. Mendelson, Introduction to mathematical logic
Risorsa bibliografica facoltativaM. Machover, Set theory, logic and their limitations
Risorsa bibliografica facoltativaK. Rosen, Discrete mathematics and its applications
Risorsa bibliografica facoltativaM. Ben-Ari, Mathematical logic for computer science
Risorsa bibliografica facoltativaD. van Dalen, Logic and structure

Software utilizzato
Nessun software richiesto

Forme didattiche
Tipo Forma Didattica Ore di attività svolte in aula
Ore di studio autonome
Laboratorio Informatico
Laboratorio Sperimentale
Laboratorio Di Progetto
Totale 50:00 75:00

Informazioni in lingua inglese a supporto dell'internazionalizzazione
Insegnamento erogato in lingua Inglese
Disponibilità di materiale didattico/slides in lingua inglese
Disponibilità di libri di testo/bibliografia in lingua inglese
Possibilità di sostenere l'esame in lingua inglese
Disponibilità di supporto didattico in lingua inglese
schedaincarico v. 1.9.1 / 1.9.1
Area Servizi ICT