SGGS: conflict-driven first-order theorem proving

Time: 14:00

Venue: LT 1.5, Kilburn Building, The University of Manchester, Oxford Road, M13 9PL

Sorry, this event has now ended.

Speaker: Prof Maria Paolo Bonacina, University of Verona

Abstract: Many problems in computer science can be encoded as instances of propositional satisfiability (SAT) and approached by SAT solvers based in 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 fit in a big picture that sees the rise of a general paradigm of conflict-driven reasoning. 

Refreshments will be served in the Kilburn Common Room from 15:00.