The \(\exists^*\forall^*\) part of the theory of ground term algebra modulo an AC symbol is undecidable. (Q1400708)
From MaRDI portal
 | This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use this page instead for the normal view: The \(\exists^*\forall^*\) part of the theory of ground term algebra modulo an AC symbol is undecidable. |
scientific article; zbMATH DE number 1964172
| Language | Label | Description | Also known as |
|---|---|---|---|
| English | The \(\exists^*\forall^*\) part of the theory of ground term algebra modulo an AC symbol is undecidable. |
scientific article; zbMATH DE number 1964172 |
Statements
The \(\exists^*\forall^*\) part of the theory of ground term algebra modulo an AC symbol is undecidable. (English)
0 references
2002
0 references
We show that the \(\exists^*\forall^*\) part of the equational theory modulo an AC symbol is undecidable. This solves the open problem 25 from the RTA list. We show that this result holds also for the equational theory modulo an ACI symbol.
0 references
unification
0 references
decidability
0 references
0.783756673336029
0 references
0.7794679403305054
0 references
