TY - JOUR

T1 - Order-sorted equational generalization algorithm revisited

AU - Alpuente, María

AU - Escobar, Santiago

AU - Meseguer, José

AU - Sapiña, Julia

N1 - Publisher Copyright:
© 2021, The Author(s), under exclusive licence to Springer Nature Switzerland AG.

PY - 2022/5

Y1 - 2022/5

N2 - Generalization, also called anti-unification, is the dual of unification. A generalizer of two terms t and t′ is a term t′′ of which t and t′ are substitution instances. The dual of most general equational unifiers is that of least general equational generalizers, i.e., most specific anti-instances modulo equations. In a previous work, we extended the classical untyped generalization algorithm to: (1) an order-sorted typed setting with sorts, subsorts, and subtype polymorphism; (2) work modulo equational theories, where function symbols can obey any combination of associativity, commutativity, and identity axioms (including the empty set of such axioms); and (3) the combination of both, which results in a modular, order-sorted equational generalization algorithm. However, Cerna and Kutsia showed that our algorithm is generally incomplete for the case of identity axioms and a counterexample was given. Furthermore, they proved that, in theories with two identity elements or more, generalization with identity axioms is generally nullary, yet it is finitary for both the linear and one-unital fragments, i.e., either solutions with repeated variables are disregarded or the considered theories are restricted to having just one function symbol with an identity or unit element. In this work, we show how we can easily extend our original inference system to cope with the non-linear fragment and identify a more general class than one–unit theories where generalization with identity axioms is finitary.

AB - Generalization, also called anti-unification, is the dual of unification. A generalizer of two terms t and t′ is a term t′′ of which t and t′ are substitution instances. The dual of most general equational unifiers is that of least general equational generalizers, i.e., most specific anti-instances modulo equations. In a previous work, we extended the classical untyped generalization algorithm to: (1) an order-sorted typed setting with sorts, subsorts, and subtype polymorphism; (2) work modulo equational theories, where function symbols can obey any combination of associativity, commutativity, and identity axioms (including the empty set of such axioms); and (3) the combination of both, which results in a modular, order-sorted equational generalization algorithm. However, Cerna and Kutsia showed that our algorithm is generally incomplete for the case of identity axioms and a counterexample was given. Furthermore, they proved that, in theories with two identity elements or more, generalization with identity axioms is generally nullary, yet it is finitary for both the linear and one-unital fragments, i.e., either solutions with repeated variables are disregarded or the considered theories are restricted to having just one function symbol with an identity or unit element. In this work, we show how we can easily extend our original inference system to cope with the non-linear fragment and identify a more general class than one–unit theories where generalization with identity axioms is finitary.

KW - Associativity

KW - Commutativity

KW - Equational reasoning

KW - Identity

KW - Least general generalization

KW - Order-Sorted

KW - Rule–based languages

UR - http://www.scopus.com/inward/record.url?scp=85115729435&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85115729435&partnerID=8YFLogxK

U2 - 10.1007/s10472-021-09771-1

DO - 10.1007/s10472-021-09771-1

M3 - Article

AN - SCOPUS:85115729435

VL - 90

SP - 499

EP - 522

JO - Annals of Mathematics and Artificial Intelligence

JF - Annals of Mathematics and Artificial Intelligence

SN - 1012-2443

IS - 5

ER -