**Instructor:**
Maria Paola Bonacina

**Class meetings:**
2:30pm - 4:30pm on Thursday February 9, Tuesday February 21, and Tuesday February 28
in classroom M, Thursday March 2 in the Sala Riunioni II floor, and Tuesday March 7
in the Sala Riunioni ground floor; total: 10hrs.

**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:**

- First lecture: Introduction to Automated Reasoning.
- Second, third, and fourth lectures: Topics in Model-Based Reasoning: Towards Integration of Proving and Solving.
- Fifth lecture: SGGS: A CDCL-like First-Order Theorem Proving Method.