SCV0847 - LOGIC FOR ARTIFICIAL INTELLIGENCE

courses

ID:

SCV0847

Duration (hours):

80

CFU:

SSD:

LOGICA MATEMATICA

Year:

2025

Date/time interval

Secondo Semestre (23/02/2026 - 29/05/2026)

Course Objectives

The course aims to provide basic knowledge of how logical systems can be used to deal with computational issues, in particular in relation with artificial intelligence and knowledge representation. 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. At the end of the course the student will be able to: 1. Know the basic logical systems, propositional and predicative logic, temporal logic and modal logic 2. Know and apply the basic SAT solvers, binary decision diagrams and their algorithms 3. Know how to write programs in logic programming (Prolog) for representing knowledge 4. Know how to deal with pure declarative programming (Answer Set Programming) for planning problems and for finding solutions to puzzles and games 5. Understand tools and properties of model checking, know and apply the NuSMV model checker 6. Know how to deal with uncertainty and vagueness in reasoning, using probabilistic and fuzzy logic Expected learning outcomes include the ability to identify any errors in computational argument, and to have the ability to use a formal language for the description of computational problems.

Course Prerequisites

Knowledge of basic concepts of discrete mathematics is required. In the course the basic notions of propositional and predicate logic will be summarized, but some prior knowledge is advisable.

Teaching Methods

56h lectures + 24h Exercises. The lessons aim at presenting multiple aspects of mathematical logic in the realm of artificial intelligence, as well as practical applications of the proposed software.

Assessment Methods

The scope of the exam is to certify that students have all knowledge and ability explained above, by evaluating the knowledge skill and the ability to understand and then to expose the logical contents of the course. The exam consists in an oral discussion during which the student has to talk on a topic chosen from a list proposed by the teacher and a written test. The two parts of the exam can be taken at different times. The seminar can also be held during the lecture period, while the written test must necessarily take place during the official exam sessions. Final mark (out of 30) depends on the completeness and correctness of the exposition (70%), the clarity of the exposition (20%) and adequateness of answers (10%).

Propositional logic, truth tables, satisfiability and validity, predicate logic, language, semantics and expressivity, clauses and resolution (8h+ 2h exercises, objective 1)
Linear temporal logic, syntax and semantics. Branching time logic (4h +2h exercises, objective 1)
SAT solvers (linear and cubic), Binary decision diagrams, algorithms for binary decision diagrams (6h+4h exercises, objective 2)
Logic programming, basic examples, recursion, lists and non-logical features, Logic for knowledge representation, SWI-PROLOG (10h + 6h exercises, objective 3)
Answer set programming, pure declarative paradigms, logic programming for solving games and puzzles, CLINGO (10 h+6h exercises, objective 4)
Model checking: Systems, tools and properties. The NuSMV model checker (10h+4h exercises, objective 5)
Probabilistic and fuzzy logic to deal with uncertainty and vagueness in reasoning (8h, objective 6)