FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Towards Generalization Methods for Purely Idempotent Equational Theories

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: