Files in this item

FilesDescriptionFormat

application/pdf

application/pdfmain.pdf (582kB)
(no description provided)PDF

Description

Title:Metalevel algorithms for variant satisfiability
Author(s):Skeirik, Stephen; Meseguer, José
Subject(s):finite variant property (FVP)
folding variant narrowing
satisfiability in initial algebras
metalevel algorithms
Maude
Abstract:Variant satisfiability is a theory-generic algorithm to decide quantifier-free satisfiability in an initial algebra when its corresponding theory 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 in Maude 2.7 of variant satisfiability using these sub-algorithms.
Issue Date:2016-06-07
Genre:Technical Report
Type:Text
Language:English
URI:http://hdl.handle.net/2142/90238
Sponsor:NSF CNS 13-19109
Date Available in IDEALS:2016-06-07


This item appears in the following Collection(s)

Item Statistics