Equational Anti-Unification over Absorption Theories

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F24%3A00584853" target="_blank" >RIV/67985807:_____/24:00584853 - isvavai.cz</a>

Result on the web

<a href="http://dx.doi.org/10.1007/978-3-031-63501-4_17" target="_blank" >http://dx.doi.org/10.1007/978-3-031-63501-4_17</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-63501-4_17" target="_blank" >10.1007/978-3-031-63501-4_17</a>

Result language

angličtina

Original language name

Equational Anti-Unification over Absorption Theories

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/GF22-06414L" target="_blank" >GF22-06414L: Proof analysis AND Automated deduction FOr REcursive STructures</a><br>

Continuities

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2024

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

Automated Reasoning. 12th International Joint Conference, IJCAR 2024. Proceedings Part II

ISBN

978-3-031-63501-4

ISSN

0302-9743

e-ISSN

1611-3349

Number of pages

21

Pages from-to

317-337

Publisher name

Springer

Place of publication

Cham

Event location

Nancy

Event date

Jul 1, 2024

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

001275062900017