Abstract
Variant satisfiability is a theory-generic algorithm to decide quantifier-free satisfiability in an initial algebra TΣ/E when the theory (Σ,E) has the finite variant property and its constructors satisfy a compactness condition. This paper: (i) gives a precise definition of several meta-level sub-algorithms needed for variant satisfiability; (ii) proves them correct; and (iii) presents a reflective implementation of variant satisfiability checking using these sub-algorithms in Maude 2.7.1.
Original language | English (US) |
---|---|
Pages (from-to) | 81-110 |
Number of pages | 30 |
Journal | Journal of Logical and Algebraic Methods in Programming |
Volume | 96 |
DOIs | |
State | Published - Apr 2018 |
Keywords
- Finite variant property (FVP)
- Folding variant narrowing
- Maude
- Metalevel algorithms
- Reflection
- Satisfiability in initial algebras
ASJC Scopus subject areas
- Theoretical Computer Science
- Software
- Logic
- Computational Theory and Mathematics