Our seminar series is free and available for anyone to attend. Unless otherwise stated, seminars take place on Wednesday afternoons at 2pm in the Kilburn Building during teaching season.

If you wish to propose a seminar speaker please contact Antoniu Pop.


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
▲ Up to the top