English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

This paper introduces GLINTS, a graphical tool for exploring variantnarrowing computations in Maude. The most recent version of Maude, version2.7.1, provides quite sophisticated unification features, includingorder-sorted equational unification for convergent theories modulo axioms suchas associativity, commutativity, and identity (ACU). This novel equationalunification relies on built-in generation of the set of 'variants' of a term$t$, i.e., the canonical form of $t \sigma$ for a computed substitution$\sigma$. 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, especiallywhen the theory satisfies the 'finite variant property', i.e., there is afinite number of most general variants for every term in the theory. However,variant narrowing computations can be extremely involved and are simplypresented in text format by Maude, often being too heavy to be debugged or evenunderstood. The GLINTS system provides support for (i) determining whether agiven theory satisfies the finite variant property, (ii) thoroughly exploringvariant narrowing computations, (iii) automatic checking of node 'embedding'and 'closedness' modulo axioms, and (iv) querying and inspecting selected partsof the variant trees. This paper is under consideration for acceptance in TPLP.

Inspecting Maude Variants with GLINTS