Nominal Equational Problems

We define nominal equational problems of the form [Formula: see text] , where [Formula: see text] consists of conjunctions and disjunctions of equations [Formula: see text] , freshness constraints [Formula: see text] and their negations: [Formula: see text] and [Image: see text], where [Formula: see text] is an atom and [Formula: see text] nominal terms. We give a general definition of solution and a set of simplification rules to compute solutions in the nominal ground term algebra. For the latter, we define notions of solved form from which solutions can be easily extracted and show that the simplification rules are sound, preserving, and complete. With a particular strategy for rule application, the simplification process terminates and thus specifies an algorithm to solve nominal equational problems. These results generalise previous results obtained by Comon and Lescanne for first-order languages to languages with binding operators. In particular, we show that the problem of deciding the validity of a first-order equational formula in a language with binding operators (i.e., validity modulo [Formula: see text] -equality) is decidable.