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.

• Type: Conference
• Year: 2009
• Where: CADE
• Authors: Matthias Horbach, Christoph Weidenbach
• Keywords: Automated Reasoning, CADE 2009, Clause Set, Satisfiable Saturated Clause, Superposition Calculus