Inspecting Maude variants with GLINTS*. Issue 5 (24th August 2017)

• Record Type: Journal Article
• Authors: ALPUENTE, M.; ESCOBAR, S.; SAPIÑA, J.; CUENCA-ORTEGA, A.
• Editors: Rocha, Ricardo; Cao Son, Tran
• Is Part Of: Theory and practice of logic programming. Volume 17:Issue 5/6(2017)
• Page Start: 689
• Page End: 707
• Publication Date: 2017-08-24
• Subjects: Rewriting Logic, -- Narrowing, -- Variant, -- Maude, -- Embedding, -- Finite Variant Property; Logic programming -- Periodicals; Artificial intelligence -- Computer programs -- Periodicals; Constraint programming (Computer science) -- Periodicals; 005.115
• DOI: 10.1017/S147106841700031X
• Languages: English
• ISSNs: 1471-0684

Abstract

Abstract: This 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 of variants of a term t, i.e., the canonical form of t σ for a computed substitution σ. Variant generation relies on a novel narrowing strategy called folding variant narrowing that opens up new applications in formal reasoning, theorem proving, testing, protocol analysis, and model checking, especially when the theory satisfies the finite 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. TheGLINTS system provides support for (i) determining whether a given theory satisfies the finite variant property, (ii) thoroughly exploring variant narrowing computations, (iii) automatic checking of node embedding and closedness modulo axioms, and (iv) querying and inspecting selected parts of the variant trees.