- -

Variant-Based Decidable Satisfiability in Initial Algebras with Predicates

RiuNet: Institutional repository of the Polithecnic University of Valencia

Share/Send to

Cited by

Statistics

Variant-Based Decidable Satisfiability in Initial Algebras with Predicates

Show simple item record

Files in this item

dc.contributor.author Gutiérrez Gil, Raúl es_ES
dc.contributor.author Meseguer, José es_ES
dc.date.accessioned 2019-08-02T20:00:52Z
dc.date.available 2019-08-02T20:00:52Z
dc.date.issued 2018 es_ES
dc.identifier.issn 0302-9743 es_ES
dc.identifier.uri http://hdl.handle.net/10251/124698
dc.description.abstract [EN] 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 (¿,E¿B) under two conditions: (i) E¿B has the finite variant property and B has a finitary unification algorithm; and (ii) (¿,E¿B) protects a constructor subtheory (¿,E¿¿B¿) 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. es_ES
dc.language Inglés es_ES
dc.publisher Springer-Verlag es_ES
dc.relation MINISTERIO DE ECONOMIA Y EMPRESA/TIN2015-69175-C4-1-R es_ES
dc.relation GENERALITAT VALENCIANA/PROMETEOII/2015/013 es_ES
dc.relation INST NAL DE CIBERSEGURIDAD DE ESPAÑA, S.A. /INCIBEI-2015-27346 es_ES
dc.relation.ispartof Lecture Notes in Computer Science es_ES
dc.rights Reserva de todos los derechos es_ES
dc.subject Finite variant property (fvp) es_ES
dc.subject OS-compactness es_ES
dc.subject User-definable predicates es_ES
dc.subject Decidable validity and satisfiability in initial algebras es_ES
dc.subject.classification LENGUAJES Y SISTEMAS INFORMATICOS es_ES
dc.title Variant-Based Decidable Satisfiability in Initial Algebras with Predicates es_ES
dc.type Artículo es_ES
dc.type Comunicación en congreso es_ES
dc.identifier.doi 10.1007/978-3-319-94460-9_18 es_ES
dc.rights.accessRights Abierto es_ES
dc.description.bibliographicCitation Gutiérrez Gil, R.; Meseguer, J. (2018). Variant-Based Decidable Satisfiability in Initial Algebras with Predicates. Lecture Notes in Computer Science. 10855:306-322. https://doi.org/10.1007/978-3-319-94460-9_18 es_ES
dc.description.accrualMethod S es_ES
dc.relation.conferencename 27th International Symposium on Logic-based Program Synthesis and Transformation (LOPSTR 2017) es_ES
dc.relation.conferencedate Octubre 10-12,2017 es_ES
dc.relation.conferenceplace Namur, Blegium es_ES
dc.relation.publisherversion https://doi.org/10.1007/978-3-319-94460-9_18 es_ES
dc.description.upvformatpinicio 306 es_ES
dc.description.upvformatpfin 322 es_ES
dc.type.version info:eu repo/semantics/publishedVersion es_ES
dc.description.volume 10855 es_ES
dc.relation.pasarela 376345 es_ES
dc.contributor.funder GENERALITAT VALENCIANA es_ES
dc.contributor.funder MINISTERIO DE ECONOMIA Y EMPRESA es_ES
dc.contributor.funder INST NAL DE CIBERSEGURIDAD DE ESPAÑA, S.A. es_ES


This item appears in the following Collection(s)

Show simple item record