The \(\exists^*\forall^*\) part of the theory of ground term algebra modulo an AC symbol is undecidable. (Q1400708)
From MaRDI portal
scientific article
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 |
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