• SGGS: conflict-driven first-order theorem proving 29/03/17 14:00 KB L.T 1.5

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


    Abstract
    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

    gravatar Karon Mee
Generated: Thursday, 14 December 2017 06:26:46
Last change: Friday, 24 March 2017 16:30:52
▲ Up to the top