Variant-Based Decidable Satisfiability in Initial Algebras with Predicates

Raúl Gutiérrez; José Meseguer

Variant-Based Decidable Satisfiability in Initial Algebras with Predicates

Programming Languages 2017-09-18 v1

Authors: Raúl Gutiérrez , José Meseguer

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 $({\Sigma},E \cup B)$ under two conditions: (i) $E \cup B$ has the finite variant property and $B$ has a finitary unification algorithm; and (ii) $({\Sigma},E \cup B)$ protects a constructor subtheory $({\Omega},E_{\Omega} \cup B_{\Omega})$ 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.

Keywords

first-order logic algebraic theory computational complexity

Cite

@article{arxiv.1709.05203,
  title  = {Variant-Based Decidable Satisfiability in Initial Algebras with Predicates},
  author = {Raúl Gutiérrez and José Meseguer},
  journal= {arXiv preprint arXiv:1709.05203},
  year   = {2017}
}

Comments

Pre-proceedings paper presented at the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017), Namur, Belgium, 10-12 October 2017 (arXiv:1708.07854)

Variant-Based Decidable Satisfiability in Initial Algebras with Predicates

Abstract

Keywords

Cite

Comments

Related papers