SGGS: Semantically-Guided Goal-Sensitive Reasoning

SGGS is a model-based conflict-driven theorem-proving method that generalizes to first-order logic the Conflict-Driven Clause Learning (CDCL) procedure for propositional satisfiability. SGGS is semantically guided by a given initial interpretation and uses a trail of constrained clauses with selected literals to represent the current candidate model, which is a modification of the initial interpretation. Until neither a refutation nor a model have been found, SGGS makes progress by either fixing the current candidate model or extending it with an instance of an input clause. Fixing the current candidate model may involve explaining and solving a conflict or removing intersections between selected literals. SGGS is refutationally complete and model-complete in the limit. These features make it attractive as a theorem-proving or model-building method, and as a basis for model-constructing decision procedures for decidable fragments in first-order or Horn logic:



Maria Paola Bonacina