Withdraw
Loading…
Variant-Based Decidable Satisfiability in Initial Algebras with Predicates
Gutiérrez, Raúl; Meseguer, José
Loading…
Permalink
https://hdl.handle.net/2142/96264
Description
- Title
- Variant-Based Decidable Satisfiability in Initial Algebras with Predicates
- Author(s)
- Gutiérrez, Raúl
- Meseguer, José
- Issue Date
- 2017-06-27
- Keyword(s)
- finite variant property (FVP)
- OS-compactness
- user-definable predicates
- decidable validity and satisfiability in initial algebras
- 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 U B) under two conditions: (i) E U B has the finite variant property and B has a finitary unification algorithm; and (ii) (Sigma,E U B) protects a constructor subtheory (Omega,E_Omega U 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.
- Type of Resource
- text
- Language
- en
- Permalink
- http://hdl.handle.net/2142/96264
Owning Collections
Manage Files
Loading…
Edit Collection Membership
Loading…
Edit Metadata
Loading…
Edit Properties
Loading…
Embargoes
Loading…