## Files in this item

FilesDescriptionFormat

application/pdf

var-pred-techreport.pdf (418kB)
(no description provided)PDF

## Description

 Title: Variant Satisfiability in Initial Algebras with Predicates Author(s): Gutierrez Raul; Meseguer Jose Subject(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. Issue Date: 2018-02-12 Genre: Technical Report Type: Text Language: English URI: http://hdl.handle.net/2142/99039 Sponsor: Partially supported by NSF Grant CNS 14-09416, NRL under contract number N00173-17-1-G002, the EU (FEDER), Spanish MINECO project TIN2015-69175-C4-1-R and GV project PROMETEOII/2015/013. Raul Gutierrez was also supported by INCIBE program Ayudas para la excelencia de los equipos de investigacion avanzada en ciberseguridad'' Date Available in IDEALS: 2018-02-12
﻿