Towards Generalization Methods for Purely Idempotent Equational Theories
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
UNIF 2018
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
In Generalisation de termes en theorie equationnelle. Cas associatif-commutatif, 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 handling generalization within idempotent equational theories.