Related papers: Nominal Equational Rewriting and Narrowing
Narrowing extends term rewriting with the ability to search for solutions to equational problems. While first-order rewriting and narrowing are well studied, significant challenges arise in the presence of binders, freshness conditions and…
Many formal languages include binders as well as operators that satisfy equational axioms, such as commutativity. Here we consider the nominal language, a general formal framework which provides support for the representation of binders,…
We analyse the relationship between nominal algebra and nominal rewriting, giving a new and concise presentation of equational deduction in nominal theories. With some new results, we characterise a subclass of equational theories for which…
Nominal logic is an extension of first-order logic which provides a simple foundation for formalizing and reasoning about abstract syntax modulo consistent renaming of bound names (that is, alpha-equivalence). This article investigates…
The recently introduced framework of Graded Quantitative Rewriting is an innovative extension of traditional rewriting systems, in which rules are annotated with degrees drawn from a quantale. This framework provides a robust foundation for…
Nominal unification calculates substitutions that make terms involving binders equal modulo alpha-equivalence. Although nominal unification can be seen as equivalent to Miller's higher-order pattern unification, it has properties, such as…
We study nominal anti-unification, which is concerned with computing least general generalizations for given terms-in-context. In general, the problem does not have a least general solution, but if the set of atoms permitted in…
Nominal unification is an extension of first-order unification that takes into account the \alpha-equivalence relation generated by binding operators, following the nominal approach. We propose a sound and complete procedure for nominal…
Narrowing is a procedure that was first studied in the context of equational E-unification and that has been used in a wide range of applications. The classic completeness result due to Hullot states that any term rewriting derivation…
Nominal Logic is a version of first-order logic with equality, name-binding, renaming via name-swapping and freshness of names. Contrarily to higher-order logic, bindable names, called atoms, and instantiable variables are considered as…
Recursive relational specifications are commonly used to describe the computational structure of formal systems. Recent research in proof theory has identified two features that facilitate direct, logic-based reasoning about such…
Nominal abstract syntax is a popular first-order technique for encoding, and reasoning about, abstract syntax involving binders. Many of its applications involve constraint solving. The most commonly used constraint solving algorithm over…
All current investigations to analyze the derivational complexity of term rewrite systems are based on a single termination method, possibly preceded by transformations. However, the exclusive use of direct criteria is problematic due to…
Logically constrained term rewriting is a relatively new formalism where rules are equipped with constraints over some arbitrary theory. Although there are many recent advances with respect to rewriting induction, completion, complexity…
We give a method to prove confluence of term rewriting systems that contain non-terminating rewrite rules such as commutativity and associativity. Usually, confluence of term rewriting systems containing such rules is proved by treating…
Nominal terms extend first-order terms with binding. They lack some properties of first- and higher-order terms: Terms must be reasoned about in a context of 'freshness assumptions'; it is not always possible to 'choose a fresh variable…
We introduce Nominal Matching Logic (NML) as an extension of Matching Logic with names and binding following the Gabbay-Pitts nominal approach. Matching logic is the foundation of the $\mathbb{K}$ framework, used to specify programming…
Rewriting is a formalism widely used in computer science and mathematical logic. The classical formalism has been extended, in the context of functional languages, with an order over the rules and, in the context of rewrite based languages,…
A method for selecting solution constructors in narrowing is presented. The method is based on a sort discipline that describes regular sets of ground constructor terms as sorts. It is extended to cope with regular sets of ground…
Nominal logic is a variant of first-order logic that provides support for reasoning about bound names in abstract syntax. A key feature of nominal logic is the new-quantifier, which quantifies over fresh names (names not appearing in any…