SGGS: Semantically-Guided Goal-Sensitive Reasoning

SGGS is a theorem-proving method that generalizes to first-order logic the Conflict-Driven Clause Learning (CDCL) procedure for propositional satisfiability: SGGS uses sequence of constrained clauses with selected literals to represent candidate models, with literal selection playing the role of decision, and a given interpretation for semantic guidance that allows it to realize first-order clausal propagation. SGGS employs instance generation to extend the model, and resolution as well as other inferences to explain and solve conflicts, repairing the candidate model. SGGS is refutationally complete and model-complete in the limit. SGGS is first order, model based, semantically guided, goal sensitive, and proof confluent, which is a rare combination:



Maria Paola Bonacina