equational unification
Recently Published Documents


TOTAL DOCUMENTS

22
(FIVE YEARS 0)

H-INDEX

5
(FIVE YEARS 0)

2020 ◽  
Vol 325 ◽  
pp. 38-51
Author(s):  
Damián Aparicio-Sánchez ◽  
Santiago Escobar ◽  
Julia Sapiña


2019 ◽  
Vol 19 (5-6) ◽  
pp. 874-890
Author(s):  
MARÍA ALPUENTE ◽  
SANTIAGO ESCOBAR ◽  
JULIA SAPIÑA ◽  
DEMIS BALLIS

AbstractConcurrent functional languages that are endowed with symbolic reasoning capabilities such as Maude offer a high-level, elegant, and efficient approach to programming and analyzing complex, highly nondeterministic software systems. Maude’s symbolic capabilities are based on equational unification and narrowing in rewrite theories, and provide Maude with advanced logic programming capabilities such as unification modulo user-definable equational theories and symbolic reachability analysis in rewrite theories. Intricate computing problems may be effectively and naturally solved in Maude thanks to the synergy of these recently developed symbolic capabilities and classical Maude features, such as: (i) rich type structures with sorts (types), subsorts, and overloading; (ii) equational rewriting modulo various combinations of axioms such as associativity, commutativity, and identity; and (iii) classical reachability analysis in rewrite theories. However, the combination of all of these features may hinder the understanding of Maude symbolic computations for non-experienced developers. The purpose of this article is to describe how programming and analysis of Maude rewrite theories can be made easier by providing a sophisticated graphical tool called Narval that supports the fine-grained inspection of Maude symbolic computations.



10.29007/65sh ◽  
2018 ◽  
Author(s):  
Santiago Escobar

Automated reasoning modulo an equational theory E is a fundamental technique in many applications. In this talk, we would present a narrowing-based equational unification algorithm for theories satisfying the finite variant property. We also talk about equational generalization, also called anti-unification



2017 ◽  
Vol 17 (5-6) ◽  
pp. 689-707 ◽  
Author(s):  
M. ALPUENTE ◽  
S. ESCOBAR ◽  
J. SAPIÑA ◽  
A. CUENCA-ORTEGA

AbstractThis paper introducesGLINTS, a graphical tool for exploring variant narrowing computations in Maude. The most recent version of Maude, version 2.7.1, provides quite sophisticated unification features, including order-sorted equational unification for convergent theories modulo axioms such as associativity, commutativity, and identity. This novel equational unification relies on built-in generation of the set ofvariantsof a termt, i.e., the canonical form oftσ for a computed substitution σ. Variant generation relies on a novel narrowing strategy calledfolding variant narrowingthat opens up new applications in formal reasoning, theorem proving, testing, protocol analysis, and model checking, especially when the theory satisfies thefinite variant property, i.e., there is a finite number of most general variants for every term in the theory. However, variant narrowing computations can be extremely involved and are simply presented in text format by Maude, often being too heavy to be debugged or even understood. TheGLINTSsystem provides support for (i) determining whether a given theory satisfies the finite variant property, (ii) thoroughly exploring variant narrowing computations, (iii) automatic checking of nodeembeddingandclosednessmodulo axioms, and (iv) querying and inspecting selected parts of the variant trees.



2012 ◽  
Vol 290 ◽  
pp. 37-50 ◽  
Author(s):  
Joe Hendrix ◽  
José Meseguer


2010 ◽  
Vol 19 (6) ◽  
pp. 731-762 ◽  
Author(s):  
M. Alpuente ◽  
S. Escobar ◽  
J. Iborra


2009 ◽  
Vol 238 (3) ◽  
pp. 103-119 ◽  
Author(s):  
Santiago Escobar ◽  
José Meseguer ◽  
Ralf Sasse


1998 ◽  
Vol 198 (1-2) ◽  
pp. 1-47
Author(s):  
Friedrich Otto ◽  
Paliath Narendran ◽  
Daniel J. Dougherty


Sign in / Sign up

Export Citation Format

Share Document