Semantically-guided goal-sensitive reasoning: inference system and completeness

We present a new method for clausal theorem proving, named SGGS from semantically-guided goal-sensitive reasoning. SGGS generalizes to first-order logic the Conflict-Driven Clause Learning (CDCL) procedure for propositional satisfiability. Starting from an initial interpretation,used for semantic guidance, SGGS employs a sequence of constrained clauses to represent a candidate model, instance generation to extend it, resolution and other inferences to explain and solve conflicts, amending the model. We prove that SGGS is refutationally complete and model complete in the limit, regardless of initial interpretation. SGGS is also goal sensitive, if the initial interpretation is properly chosen, and proof confluent, because it repairs the current model without undoing steps by backtracking. Thus, SGGS is a complete first-order methodthat is simultaneously model-based `a la CDCL, semantically-guided, goal-sensitive, and proof confluent.