Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6874850 | Journal of Logical and Algebraic Methods in Programming | 2018 | 30 Pages |
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.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Stephen Skeirik, José Meseguer,