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.
Semantically-guided goal-sensitive reasoning: inference system and completeness
BONACINA, Maria Paola
;
2017-01-01
Abstract
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.File | Dimensione | Formato | |
---|---|---|---|
JAR2017sggs-inference.pdf
accesso aperto
Descrizione: Articolo principale
Tipologia:
Documento in Post-print
Licenza:
Creative commons
Dimensione
371.33 kB
Formato
Adobe PDF
|
371.33 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.