Unification under associativity and idempotence is of type nullary (Q580999): Difference between revisions
From MaRDI portal
Added link to MaRDI item. |
Removed claim: author (P16): Item:Q1110492 |
||
Property / author | |||
Property / author: Manfred Schmidt-Schauss / rank | |||
Revision as of 06:04, 22 February 2024
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