Unification under associativity and idempotence is of type nullary (Q580999)

From MaRDI portal
scientific article
Language Label Description Also known as
English
Unification under associativity and idempotence is of type nullary
scientific article

    Statements

    Unification under associativity and idempotence is of type nullary (English)
    0 references
    0 references
    1986
    0 references
    Unification is concerned with solving equations given an equational theory. An important problem is to find representative sets of most general unifiers (solutions) for particular equational theories. In the paper it is shown that free idempotent semigroups (bands) including free constants have unification type zero. An example is constructed such that every complete set of unifiers contains redundant unifiers. This is the first known natural equational theory with this property.
    0 references
    0 references
    theorem proving
    0 references
    equational theory
    0 references
    free idempotent semigroups
    0 references
    bands
    0 references
    unification type zero
    0 references
    0 references
    0 references
    0 references