Semantically-Guided Goal-Sensitive Reasoning: Model Representation

SGGS (Semantically-Guided Goal-Sensitive reasoning) is a clausal theorem-proving method, which generalizes to first-order logic the Davis-Putnam-Loveland-Logemann procedure with conflict-driven clause learning (DPLL-CDCL). SGGS starts from an initial interpretation, and works towards modifying it into a model of a given set of clauses, reporting unsatisfiability if there is no model. The state of the search for a model is described by a structure, called SGGS clause sequence. We present SGGS clause sequences as a formalism to represent models; and we prove their properties related to the mechanisms of SGGS for clausal propagation, conflict solving, and conflict-driven model repair at the first-order level.