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.
Maria Paola Bonacina