Unification in commutative semigroups (Q1383954): Difference between revisions

From MaRDI portal
Added link to MaRDI item.
RedirectionBot (talk | contribs)
Removed claims
Property / author
 
Property / author: Q288794 / rank
Normal rank
 
Property / reviewed by
 
Property / reviewed by: Grigori I. Zhitomirski / rank
Normal rank
 

Revision as of 20:28, 9 February 2024

scientific article
Language Label Description Also known as
English
Unification in commutative semigroups
scientific article

    Statements

    Unification in commutative semigroups (English)
    0 references
    26 August 1998
    0 references
    Let \(V\) be a variety of algebras and \(X\) a fixed set of variables. Every function \(\sigma\) assigning \(V\)-terms to variables is called a substitution. If \(p\) is a term and \(\sigma\) is a substitution, the term \(\sigma(p)\) is defined in the usual way. Let \(\Sigma\) be a finite set of equations over \(V\). A substitution \(\sigma\) is said to be a unifier of \(\Sigma\), if for every equation \(p\approx q\in\Sigma\), the equation \(\sigma(p)\approx\sigma(q)\) holds in \(V\). The problem is to describe the structure of the set \(U(\Sigma,V)\) of all unifiers of \(\Sigma\). Speaking non-formally, it means that we want to describe all solutions of finite sets of equations, defining if every solution comes from a most general solution, and if so, defining how many most general solutions are needed to generate all solutions. This problem is solved for all varieties of commutative semigroups. A unifier \(\sigma_1\) is called more general than a unifier \(\sigma_2\) (\(\sigma_1\leq\sigma_2\)) if \(\sigma_2=\tau\sigma_1\) for some substitution \(\tau\). One of the results obtained states that every nontrivial variety \(V\) of commutative semigroups has finitary unification type (it means that all unifiers are generated, relative to \(\leq\), by a finite number of most general unifiers), unless \(V\) is the variety of abelian groups of exponent \(r>1\) or the variety of nullsemigroups, in which cases the unification type is unitary. Another result states that for commutative semigroups the unification problem is solvable. The author assumes that this is the first so general result in the area.
    0 references
    unification types
    0 references
    varieties of commutative semigroups
    0 references
    automated theorem proving
    0 references
    finite sets of equations
    0 references

    Identifiers