Semantically-guided goal-sensitive theorem proving
Maria Paola Bonacina, David A. Plaisted · 2014
We present a new inference system for first-order logic, named SGGS, which stands for semantically-guided goal-sensitive theorem proving. SGGS generalizes the model-based reasoning of the Davis-Putnam-Logemann-Loveland (DPLL) procedure. Starting from an initial interpretation, which makes it semantically guided, SGGS uses a sequence of constrained clauses to represent a current model, instance generation to extend it, and resolution and other inferences to amend it. SGGS employs unification to avoid enumerating ground terms, and it is proof confluent, so that it does not need backtracking. We prove that SGGS is refutationally complete, by showing that it is guaranteed to find a contradiction whenever the input clause set is unsatisfiable, and goal sensitive, if the initial interpretation is properly chosen. Thus, SGGS