PhD in Computer Science

PhD Course on Special Topics in Artificial Intelligence Model-based Reasoning

February 7,9,14,21,23, 28

Academic staff
Maria Paola Bonacina

Series to which this belongs

29° ciclo
30° ciclo
31° Ciclo
32° Ciclo


Objective and motivation: Logic-based artificial intelligence (AI) and specifically automated reasoning (AR) are based on the notion that complex knowledge can be represented in symbols in
the computer memory. This is why AI overlaps substantially with symbolic computation, much of AI involves symbol crunching, and AR is also called symbolic reasoning. A classical challenge in AI and AR is to inject semantics in the symbolic computation in such a way to balance the brute-force
symbol crunching with some kind of semantic guidance that embodies an understanding of the meaning of the symbols. In automated theorem proving, the notion of semantic guidance is almost
as old as theorem proving itself, as suggested, for instance, in semantic resolution, hyperresolution, or resolution with set of support. A reasoning strategy is deemed semantically guided, if it uses a fixed Herbrand interpretation to guide the search for a proof. In the neighbor field of SAT solving, where SAT stands for propositional satisfiability, approaches based on local search, or on binary decision diagrams, have been largely superseded first by the Davis-Putnam-Logemann-Loveland (DPLL) procedure, and then by the Conflict-Driven Clause Learning (CDCL) procedure. These SAT-solving procedures, and especially CDCL, are model-based, meaning that the procedure builds a candidate model, and the inferences are geared towards updating the candidate model, so that search for a model and inferences help each other. From the astounding success of CDCL-based SAT solvers arose the challenge of realizing such a mechanism in first-order logic. In recent work with David A. Plaisted, the instructor proposed a method, called SGGS, for Semantically-Guided Goal-Sensitive reasoning, that lifts CDCL to first-order logic. This advanced seminar will be an opportunity to learn about model-based reasoning and SGGS. In order to get everyone on board, the class will start with an introduction to automated reasoning, followed by an introduction to model-based automated reasoning, before delving into the advanced topics.
Class activity: The course will start with a series of lectures by the instructor followed by a series of discussion sessions. Each discussion session is organized in one of two ways: either presentation of a paper by a student, followed by discussion, followed by presentation of supple- mentary material by the instructor; or presentation of introductory material by the instructor, followed by presentation of a paper by a student, followed by discussion. The choice between the two formats will be made based on the topic. The decision on how many hours will be lectures and how many hours will be discussion sessions depends on the number of students attending the class. Therefore, the balance between the two will be finalized after the first day of the class.


  • pdf   Flyer   (pdf, it, 76 KB, 23/01/17)