Equational Anti-Unification over Absorption Theories

Kód výsledku v 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>

Výsledek na webu

<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>

Jazyk výsledku

angličtina

Název v původním jazyce

Equational Anti-Unification over Absorption Theories

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Equational Anti-Unification over Absorption Theories

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

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

Projekt

<a href="/cs/project/GF22-06414L" target="_blank" >GF22-06414L: Analýza důkazů a automatická dedukce pro rekurzivní struktury</a><br>

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2024

Kód důvěrnosti údajů

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

Název statě ve sborníku

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

ISBN

978-3-031-63501-4

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

21

Strana od-do

317-337

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Nancy

Datum konání akce

1. 7. 2024

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001275062900017