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

Research output: Contribution to book/Conference proceedings/Anthology/ReportConference contributionContributedpeer-review

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

Original languageEnglish
Title of host publication10th International Conference on Formal Structures for Computation and Deduction, FSCD 2025
EditorsMaribel Fernandez
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
ISBN (electronic)9783959773744
Publication statusPublished - 7 Jul 2025
Peer-reviewedYes

Publication series

SeriesLeibniz International Proceedings in Informatics, LIPIcs
Volume337
ISSN1868-8969

Conference

Title10th International Conference on Formal Structures for Computation and Deduction
Abbreviated titleFSCD 2025
Conference number10
Duration14 - 20 July 2025
Website
LocationEdgbaston Park Hotel and Conference Centre & Online
CityBirmingham
CountryUnited Kingdom

External IDs

ORCID /0000-0002-4049-221X/work/191036346

Keywords

ASJC Scopus subject areas

Keywords

  • Equational theories, Instantiation preorder, Modal and Description Logics, Unification type