Authors: David Cerna and Temur Kutsia
Paper Information
Title: | Towards Generalization Methods for Purely Idempotent Equational Theories |
Authors: | David Cerna and Temur Kutsia |
Proceedings: | UNIF Extended abstracts |
Editors: | Mauricio Ayala-Rincon and Philippe Balbiani |
Keywords: | Idempontent, Anti-unification, equational theories |
Abstract: | 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. |
Pages: | 5 |
Talk: | Jul 07 16:30 (Session 31S: Nominal Unification and Formalisations) |
Paper: |