Combining Generalization Algorithms in Regular Collapse-Free Theories

Result code in 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>

Result on the web

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

Result language

angličtina

Original language name

Combining Generalization Algorithms in Regular Collapse-Free Theories

Original language description

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.

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

2025

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

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

—

Number of pages

18

Pages from-to

7

Publisher name

Schloss Dagstuhl – Leibniz-Zentrum für Informatik

Place of publication

Dagstuhl

Event location

Birmingham

Event date

Jul 14, 2025

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

001594385200007