The Unification Type of an Equational Theory May Depend on the Instantiation Preorder

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragenBegutachtung

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

OriginalspracheEnglisch
Titel10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025
Redakteure/-innenMaribel Fernandez
Herausgeber (Verlag)Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (elektronisch)9783959773744
PublikationsstatusVeröffentlicht - 7 Juli 2025
Peer-Review-StatusJa

Publikationsreihe

ReiheLeibniz International Proceedings in Informatics, LIPIcs
Band337
ISSN1868-8969

Konferenz

Titel10th International Conference on Formal Structures for Computation and Deduction
KurztitelFSCD 2025
Veranstaltungsnummer10
Dauer14 - 20 Juli 2025
Webseite
OrtEdgbaston Park Hotel and Conference Centre & Online
StadtBirmingham
LandGroß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