非表示:
キーワード:
-
要旨:
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.
