SGGS: Model-Based First-Order Theorem Proving

is a new inference system for first-order logic. It was inspired
by the idea of generalizing the model-based style of the
Davis-Putnam-Logemann-Loveland (DPLL) procedure, which is a key
feature of SAT solvers, SMT solvers, and model-constructing
decision procedures for specific theories. Model-based reasoning
in first-order logic is challenging: SGGS uses a given interpretation
for semantic guidance; avoids backtracking, because it is proof
confluent; is refutationally complete; and it is goal-sensitive,
if the initial interpretation is properly chosen. In terms of
operations, SGGS combines instance generation, resolution, and
constraints, in a model-centric approach: it uses sequences of
constrained clauses to represent models, instance generation to
extend the model, resolution and other inferences to repair it.
This talk advertises SGGS presenting the main ideas that make its
seemingly rare combination of properties possible.

(Joint work with David A. Plaisted)