ABSTRACT. We consider the problem of unification modulo an equational theory ACh, which consists of a function h which is homomorphic over an associative-commutative operator +. Unification modulo ACh is undecidable, so we define a bounded ACh unification problem. In this bounded version of ACh unification we essentially bound the number of times h can be recursively applied to a term, and only allow solutions that satisfy this bound. There is no bound on the number of occurrences of h in a term, and the + symbol can be applied an unlimited number of times. We give inference rules for solving bounded ACh unification, and we prove that the rules are sound, complete and terminating. We have implemented the algorithm in Maude and give experimental results. We argue that this algorithm is useful in cryptographic protocol analysis.

ABSTRACT. In “Generalisation de termes en theorie equationnelle. Cas associatif-commut- atif”, a pair of terms was presented over the language { f (·, ·), g(·, ·), a, b}, where f and g are interpreted over an idempotent equational theory, i.e. g(x, x) = x and f (x, x) = x, resulting in an infinite set of generalizations. While this result provides an answer to the complexity of the idempotent generalization problem for arbitrarily idempotent equational theories (theories with two or more idempotent functions) the complexity of generalization for equational theories with a single idempotent function symbols was left unsolved. We show that the two idempotent function symbols example can be encoded using a single idempotent function and two uninterpreted constants thus proving that idempotent generalization, even with a single idempotent function symbol, can result in an infinite set of generalizations. Based on this result we discuss approaches to the handling generalization within idempotent equational theories.

ABSTRACT. Proximity relations are reflexive and symmetric fuzzy binary relations. They generalize similarity relations (similarity, in itself, is a generalization of equivalence in fuzzy setting) and have been introduced to deal with certain limitations of latter, related to incorrect representation of fuzzy information in some cases.

Following [1], we consider signatures where some function symbols are allowed to be in a proximity relation with each other. In our opinion, such a representation is more adequate than similarity to deal with possible mismatches between the names of symbols. Our terms are first-order terms, and the proximity relation is extended to them. In [1], a unification algorithm has been introduced for such terms. The problem we deal in this paper is a dual one: We are looking for generalizations, which, roughly, means that for two terms t1 and t2 we want to find a term r such that there exist substitution instances of r which are 'close enough to' (i.e., are in the given proximity relation with) t1 and t2.

Interestingly, the problem of computing a minimal complete set of generalizations with respect to a given proximity relation requires computing all possible maximal vertex-clique partitions in an undirected graph. We develop an algorithm for the all maximal clique partition problem, which is optimal in the sense that, first, it computes each maximal clique partition only once and, second, avoids generating and discarding false answers. Based on this method, we show that proximity-based anti-unification has the finitary type and develop a terminating, sound, and complete algorithm for computing a minimal complete set of generalizations.

[1] P. Julián-Iranzo and C. Rubio-Manzano. Proximity-based unification theory. Fuzzy Sets and Systems 262 (2015) 21–43.

ABSTRACT. Topological logics are formalisms for reasoning about topological relations between regions. In this paper, we introduce a new inference problem for topological logics, the unifiability problem, which extends the validity problem by allowing one to replace variables by terms before testing for validity. Our main result is that, within the context of the mereotopology of all regular closed polygons of the real plane, unifiable formulas always have finite complete sets of unifiers.

ABSTRACT. We consider rewriting, critical pairs and confluence tests on rewrite rules using nominal notation. Computing critical pairs is done using nominal unification, and rewriting using nominal matching. The progress is that we permit atom variables in the notation and in the unification algorithm, which generalizes previous approaches using usual nominal unification

ABSTRACT. It is well-known that the unification problem for a binary associative-commutative-idempotent function symbol with a unit (ACUI-unification) is polynomial for unification with constants and in NP for general unification. We show that the same is true if we add a finite set of ground identities.

ABSTRACT. We study decision procedures for two knowledge problems critical to the verification of security protocols, namely the intruder deduction and the static equivalence problems. These problems can be related to particular forms of context matching and context unification. Both problems are defined with respect to an equational theory and are known to be decidable when the equational theory is given by a subterm convergent term rewrite system. In this note we extend this to consider a subterm convergent equational term rewrite system defined modulo an equational theory, like Commutativity or Associativity-Commutativity. We show that for certain classes of such equational theories, namely the shallow classes, the two knowledge problems remain decidable.

ABSTRACT. At this time we only submit the abstract, which I uploaded under paper

ABSTRACT. We present a new formalization in the Isabelle proof assistant of first-order syntactic unification, including a proof of termination.

ABSTRACT. We present a nominal unification algorithm that runs in O(n × G(n)) time, where G is the functional inverse of Ackermann’s function. Nominal unification generates a set of variable assignments, if there exists one, that makes terms involving binding operations α-equivalent. We preserve names while using special representations of de Bruijn numbers. Operations on name handling, i.e., deciding the α-equivalence of two names and inferring a name that α-equals to a given one, are in constant time. To reduce an arbitrary unification problem to such name handlings, we preprocess the unification terms with the idea of Martelli-Montanari.