Combining Generalization Algorithms in Regular Collapse-Free Theories

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F25%3A00639500" target="_blank" >RIV/67985807:_____/25:00639500 - isvavai.cz</a>

Výsledek na webu

<a href="https://doi.org/10.4230/LIPIcs.FSCD.2025.7" target="_blank" >https://doi.org/10.4230/LIPIcs.FSCD.2025.7</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.4230/LIPIcs.FSCD.2025.7" target="_blank" >10.4230/LIPIcs.FSCD.2025.7</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Combining Generalization Algorithms in Regular Collapse-Free Theories

Popis výsledku v původním jazyce

We look at the generalization problem modulo some equational theories. This problem is dual to the unification problem: given two input terms, we want to find a common term whose respective two instances are equivalent to the original terms modulo the theory. There exist algorithms for finding generalizations over various equational theories. We focus on modular construction of equational generalization algorithms for the union of signature-disjoint theories. Specifically, we consider the class of regular and collapse-free theories, showing how to combine existing generalization algorithms to produce specific solutions in these cases. Additionally, we identify a class of theories that admit a generalization algorithm based on the application of axioms to resolve the problem. To define this class, we rely on the notion of syntactic theories, a concept originally introduced to develop unification procedures similar to the one known for syntactic unification. We demonstrate that syntactic theories are also helpful in developing generalization procedures similar to those used for syntactic generalization.

Název v anglickém jazyce

Combining Generalization Algorithms in Regular Collapse-Free Theories

Popis výsledku anglicky

We look at the generalization problem modulo some equational theories. This problem is dual to the unification problem: given two input terms, we want to find a common term whose respective two instances are equivalent to the original terms modulo the theory. There exist algorithms for finding generalizations over various equational theories. We focus on modular construction of equational generalization algorithms for the union of signature-disjoint theories. Specifically, we consider the class of regular and collapse-free theories, showing how to combine existing generalization algorithms to produce specific solutions in these cases. Additionally, we identify a class of theories that admit a generalization algorithm based on the application of axioms to resolve the problem. To define this class, we rely on the notion of syntactic theories, a concept originally introduced to develop unification procedures similar to the one known for syntactic unification. We demonstrate that syntactic theories are also helpful in developing generalization procedures similar to those used for syntactic generalization.

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í

2025

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

10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). LIPICs Proceedings, vol. 337

ISBN

978-3-95977-374-4

ISSN

1868-8969

e-ISSN

—

Počet stran výsledku

18

Strana od-do

7

Název nakladatele

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Místo vydání

Dagstuhl

Místo konání akce

Birmingham

Datum konání akce

14. 7. 2025

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

WRD - Celosvětová akce

Kód UT WoS článku

001594385200007