Computational Logic

Prof. Silvio Ghilardi

Bachelor in Artificial Intelligence - a.a. 2021/2022


The course is hosted at the Kiro platform of the University of Pavia. Students should register into such platform in order to download course notes, suggestions for exercises, websites for downloading software tools, advices, daily information, etc.

The first lecture will take place on Wednesday, September 29. The room of the course is Aula V1, via Venezian (for the first week only, lectures will be exceptionally hosted in Aula 405, via Celoria 20). Labs will take place at the Computer Science Department, via Celoria 18.


Aim of the course | Program | Timetable

  • Aim of the course
  • At the end of the course, students will acquire expertise in formalizing various (constraint, puzzle, planning, verification, etc.) problems in the language of symbolic logic. They will also be supposed to manage appropriate tools (basically SAT and SMT solvers) in order to get the desired solutions. At the same time, students will acquire knowledge about the involved algorithms and their heuristics.


  • Program
    1. Propositional logic and SAT problems.
    2. Resolution Calculus.
    3. DPPL procedure and related heuristics (backjumping, conflict driven clause learning).
    4. Tarski semantics for first order logic.
    5. Herbrand Theorem and ground resolution.
    6. Examples of decision procedures for quantifier-free fragments of first order theories (congruence closure, etc.)
    7. DPLL modulo theories.
    8. Combination of decision procedures.
    9. The SMT-LIB2 standard.
    10. The tool z3; Python API for z3.
    11. Examples of decision procedures for quantified fragments.


  • Timetable
  • Office hour of prof. Ghilardi: Friday 11.30, via Saldini 50 (Department of Mathematics).


    last update: 23/9/2021