Unification under associativity and idempotence is of type nullary (Q580999): Difference between revisions
From MaRDI portal
Changed an Item |
Set profile property. |
||
| Property / MaRDI profile type | |||
| Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Revision as of 00:42, 5 March 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
