Equational Anti-Unification over Absorption Theories (accepted)

0584853 - ÚI 2025 eng C - Conference Paper (international conference)
Ayala-Rincón, M. - Cerna, David M. - Barragán, A. F. G. - Kutsia, T.
Equational Anti-Unification over Absorption Theories (accepted).
IJCAR 2024 Proceedings (to appear). 2024.
[IJCAR 2024: International Joint Conference on Automated Reasoning /12./. Nancy (FR), 01.07.2024-06.07.2024]
R&D Projects: GA ČR(CZ) GF22-06414L
Institutional support: RVO:67985807

Interest in anti-unification, the dual problem of unification, is on the rise due to applications within the field of software analysis and related areas. For example, anti-unification-based techniques have found uses within clone detection and automatic program repair methods. While syntactic forms of anti-unification are enough for many applications, some aspects of software analysis methods are more appropriately modeled by reasoning modulo an equational theory. Thus, extending existing anti-unification methods to deal with important equational theories is the natural step forward. This paper considers anti-unification modulo pure absorption theories, i.e., some operators are associated with a special constant satisfying the axiom f(x,εf)≈f(εf,x)≈εf. We provide a sound and complete rule-based algorithm for such theories. Furthermore, we show that anti-unification modulo absorption is infinitary. Despite this, our algorithm terminates and produces a finitary algorithmic representation of the minimal complete set of solutions. We also show that the linear variant is finitary.
Permanent Link: https://hdl.handle.net/11104/0352643


Research data: Preprint - ArXiv.org