The Unification Type of an Equational Theory May Depend on the Instantiation Preorder
Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/Gutachten › Beitrag in Konferenzband › Beigetragen › Begutachtung
Beitragende
Abstract
The unification type of an equational theory is defined using a preorder on substitutions, called the instantiation preorder, whose scope is either restricted to the variables occurring in the unification problem, or unrestricted such that all variables are considered. It has been known for more than three decades that the unification type of an equational theory may vary, depending on which instantiation preorder is used. More precisely, it was shown in 1991 that the theory ACUI of an associative, commutative, and idempotent binary function symbol with a unit is unitary w.r.t. the restricted instantiation preorder, but not unitary w.r.t. the unrestricted one. In 2016 this result was strengthened by showing that the unrestricted type of this theory also cannot be finitary. Here, we considerably improve on this result by proving that ACUI is infinitary w.r.t. the unrestricted instantiation preorder, thus precluding type zero. We also show that, w.r.t. this preorder, the unification type of ACU (where idempotency is removed from the axioms) and of AC (where additionally the unit is removed) is infinitary, though it is respectively unitary and finitary in the restricted case. In the other direction, we prove (using the example of unification in the description logic EL) that the unification type may actually improve from type zero to infinitary when switching from the restricted instantiation preorder to the unrestricted one. In addition, we establish some general results on the relationship between the two instantiation preorders.
Details
| Originalsprache | Englisch |
|---|---|
| Titel | 10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025 |
| Redakteure/-innen | Maribel Fernandez |
| Herausgeber (Verlag) | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
| ISBN (elektronisch) | 9783959773744 |
| Publikationsstatus | Veröffentlicht - 7 Juli 2025 |
| Peer-Review-Status | Ja |
Publikationsreihe
| Reihe | Leibniz International Proceedings in Informatics, LIPIcs |
|---|---|
| Band | 337 |
| ISSN | 1868-8969 |
Konferenz
| Titel | 10th International Conference on Formal Structures for Computation and Deduction |
|---|---|
| Kurztitel | FSCD 2025 |
| Veranstaltungsnummer | 10 |
| Dauer | 14 - 20 Juli 2025 |
| Webseite | |
| Ort | Edgbaston Park Hotel and Conference Centre & Online |
| Stadt | Birmingham |
| Land | Großbritannien/Vereinigtes Königreich |
Externe IDs
| ORCID | /0000-0002-4049-221X/work/191036346 |
|---|
Schlagworte
ASJC Scopus Sachgebiete
Schlagwörter
- Equational theories, Instantiation preorder, Modal and Description Logics, Unification type