SGGS, for Semantically-Guided Goal-Sensitive reasoning, is a new reasoning method that generalizes to first-order logic the Conflict-Driven Clause Learning (CDCL) procedure of SAT solvers, SMT solvers, and model-constructing decision procedures (MCsat). Lifting CDCL to first-order logic is challenging: this talk explains why and how SGGS meets the challenge. SGGS uses a sequence of constrained clauses with selected literals to represent a candidate model, and a given interpretation for semantic guidance and to make first-order clausal propagation possible. SGGS extends the candidate model by instance generation with literal selection playing the role of decision, and mirrors CDCL in applying resolution and other inferences to repair the model upon conflict. We proved that SGGS is refutationally complete and model-complete in the limit.

(Joint work with David A. Plaisted)