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
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
theorem proving
0 references
equational theory
0 references
free idempotent semigroups
0 references
bands
0 references
unification type zero
0 references
