Towards Generalization Methods for Purely Idempotent Equational Theories

Beschreibung

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.

Zeitraum	07 Juli 2018
Ereignistitel	UNIF 2018
Veranstaltungstyp	Konferenz
Ort	Großbritannien/Vereinigtes KönigreichAuf Karte anzeigen