SGGS: conflict-driven first-order theorem proving 29/03/17 14:00 KB L.T 1.5Published: Friday, 24 March 2017
SGGS: conflict-driven first-order theorem proving 29/03/17 14:00 KB L.T 1.5 Professor Maria Paola Bonancina
SGGS: conflict-driven first-order theorem proving
Speaker: Prof Maria Paola Bonacina (University of Verona)
Host: Renate Schmidt
29th March 2017 at 14:00 in Kilburn L.T 1.5
Many problems in computer science can be encoded as instances of propositional satisfiability (SAT) and approached by SAT solvers based on the Conflict-Driven
Clause Learning (CDCL) procedure. However, the higher expressive power of first-order logic is often needed. SGGS, for Semantically-Guided Goal-Sensitive reasoning,
lifts CDCL to first-order logic. SGGS uses a sequence of constrained clauses to represent a candidate model with literal selection playing the role of decision.
A given interpretation provides semantic guidance and makes first-order clausal propagation possible. SGGS extends the candidate model by instance generation,
and when a conflict arises, SGGS explains it by resolution and solves it repairing the model in a conflict-driven manner. SGGS is refutationally complete and model-complete in the limit. SGGS fits in a big picture that sees the rise of a general paradigm of conflict-driven reasoning.
(Joint work with David A. Plaisted)
Refreshments will be served in the Staff CommonRoom from 3pm