ausblenden:
Schlagwörter:
-
Zusammenfassung:
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.
Based on an extension of our superposition calculus for fixed domains
with syntactic disequality constraints in a non-equational setting, we
describe models given by ARM (Atomic Representations of term Models) or
DIG (Disjunctions of Implicit Generalizations) representations as
minimal models of finite saturated clause sets. This allows us to
present several new decidability results for validity in such models.
These results extend in particular the known decidability results for
ARM and DIG representations.
