A note on unification type zero

DOI10.1016/0020-0190(88)90098-1MaRDI QIDQ1098285zbMATH OpenOpenAlexDBLPWikidataFDO

Authors Franz Baader

Publication date 1988

Published in Information Processing Letters (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0020-0190(88)90098-1

zbMATH Keywords

equational theoryidempotent semigroupsterm rewriting systemsunification

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Varieties and pseudovarieties of semigroups (20M07) Grammars and rewriting systems (68Q42)

Review text

An equational theory E is of unification type zero if there exist terms s, t for which there is no minimal complete set of E-unifiers of s, t. The existence of such a theory E was conjectured by Plotkin in 1972. The first example of a theory of this type was constructed by Fages and Huet in 1983. The present paper shows that the theory of idempotent semigroups is of unification type zero. This yields an example of a theory of type zero which is more natural than the example given by Fages and Huet.

Recommendations

• The theory of idempotent semigroups is of unification type zero
• Unification in varieties of idempotent semigroups
• Unification under associativity and idempotence is of type nullary
• Characterizations of unification type zero
• Unification in commutative theories

Cites work

• Complete sets of unifiers and matchers in equational theories
• scientific article; zbMATH DE number 3867289 (Why is no real title available?)
• scientific article; zbMATH DE number 4041328 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• The theory of idempotent semigroups is of unification type zero
• Unification in varieties of idempotent semigroups
• Unification under associativity and idempotence is of type nullary

Cited in

(8)

• Unification in varieties of idempotent semigroups
• Anti-unification and the theory of semirings
• What is essential unification?
• Characterizations of unification type zero
• E-unification based on generalized embedding
• Unification under associativity and idempotence is of type nullary
• Unification in varieties of completely regular semigroups
• Restricted unification in the DL \(\mathcal{FL}_0\)

This page was built for publication: A note on unification type zero

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1098285)