Sciweavers

CADE
2009
Springer

Decidability Results for Saturation-Based Model Building

14 years 4 months ago
Decidability Results for Saturation-Based Model Building
Abstract. Saturation-based calculi such as superposition can be successfully instantiated to decision procedures for many decidable fragments of first-order logic. In case of termination without generating an empty clause, a saturated clause set implicitly represents a minimal model for all clauses, based on the underlying term ordering of the superposition calculus. In general, it is not decidable whether a ground atom, a clause or even a formula holds in this minimal model of a satisfiable saturated clause set. We extend our superposition calculus for fixed domains with syntactic disequality constraints in a non-equational setting. Based on this calculus, we present several new decidability results for validity in the minimal model of a satisfiable finitely saturated clause set that in particular extend the decidability results known for ARM (Atomic Representations of term Models) and DIG (Disjunctions of Implicit Generalizations) model representations.
Matthias Horbach, Christoph Weidenbach
Added 23 Nov 2009
Updated 23 Nov 2009
Type Conference
Year 2009
Where CADE
Authors Matthias Horbach, Christoph Weidenbach
Comments (0)