Variant-Based Decidable Satisfiability in Initial Algebras with Predicates

Abstract Decision procedures can be either theory-specific, e. g. , Presburger arithmetic, or theory-generic, applying to an infinite number of user-definable theories. Variant satisfiability is a theory-generic procedure for quantifier-free satisfiability in the initial algebra of an order-sorted equational theory \((\varSigma, E \cup B)\) under two conditions: (i) \(E \cup B\) has the finite variant property and B has a finitary unification algorithm; and (ii) \((\varSigma, E \cup B)\) protects a constructor subtheory \((\varOmega, E_{\varOmega } \cup B_{\varOmega })\) that is OS- compact. These conditions apply to many user-definable theories, but have a main limitation: they apply well to data structures, but often do not hold for user-definable predicates on such data structures. We present a theory-generic satisfiability decision procedure, and a prototype implementation, extending variant-based satisfiability to initial algebras with user-definable predicates under fairly general conditions.

Authors

• Raúl Gutiérrez
• José Meseguer 0001

Keywords

No keywords are indexed for this paper.