[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
Originator: Ralf Treinen [Tre90]
Date: April 1991
Summary: Is the Σ_{2}-fragment of the first-order theory of ground terms modulo AC decidable?
Consider a finite set of function symbols containing at least one AC (associative-commutative) function symbol. Let T be the corresponding set of terms (modulo the AC properties). It is known from [Tre92] that the first-order theory (Σ_{3} fragment) of T is undecidable when F contains at least a non-constant symbol (besides the AC symbol). When F only contains an AC symbol and constants, the theory reduces to Presburger’s arithmetic and is hence decidable. On the other hand the Σ_{1} fragment of T is always decidable [Com93]. The decidability of the Σ_{2} fragment of the theory of T remains open.
Even more, the solvability of the following important particular case is open: given t,t_{1},…,t_{n} ∈ T(F,X), is there an instance of t which is not an instance of t_{1},…,t_{n} modulo the AC axioms? This is known as complement problems modulo AC.
Several special cases have been solved [Fer93][LM93], and in unpublished work in progress.
The undecidability of the Σ_{2}-fragment of the first-order theory of ground terms modulo AC has been shown by [Mar99].
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |