[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #25 (Solved !)

Originator: Ralf Treinen [Tre90]
Date: April 1991

Summary: Is the Σ₂-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 (Σ₃ 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 Σ₁ fragment of T is always decidable [Com93]. The decidability of the Σ₂ fragment of the theory of T remains open.

Remark

Even more, the solvability of the following important particular case is open: given t,t₁,…,t_n ∈ T(F,X), is there an instance of t which is not an instance of t₁,…,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 Σ₂-fragment of the first-order theory of ground terms modulo AC has been shown by [Mar99].

References

[Com93]

Hubert Comon. Complete axiomatizations of some quotient term algebras. Theoretical Computer Science, 118(2), September 1993.

[Fer93]

Maribel Fernández. AC-complement problems: Validity and negation elimination. In Claude Kirchner, editor, 5th International Conference on Rewriting Techniques and Applications, volume 690 of Lecture Notes in Computer Science, pages 358–373, Montreal, Canada, June 1993. Springer-Verlag.

[LM93]

D. Lugiez and J.-L. Moysset. Complement problems and tree automata in AC-like theories. In Proceedings of the Symposium on Theoretical Aspects of Computer Science (Würzburg, Germany), Lecture Notes in Computer Science, Berlin, 1993. Springer-Verlag.

[Mar99]

Jerzy Marcinkowski. Undecidability of the ∃^*∀^* part of the theory of ground term algebra modulo an AC symbol. In Paliath Narendran and Michael Rusinowitch, editors, 10th International Conference on Rewriting Techniques and Applications, volume 1631 of Lecture Notes in Computer Science, pages 92–102, Trento, Italy, July 1999. Springer-Verlag.

[Tre90]

Ralf Treinen. A new method for undecidability proofs of first order theories. In K. V. Nori and C. E. Veni Madhavan, editors, Proceedings of the Tenth Conference on Foundations of Software Technology and Theoretical Computer Science, volume 472 of Lecture Notes in Computer Science, pages 48–62. Springer-Verlag, 1990.

[Tre92]

Ralf Treinen. A new method for undecidability proofs of first order theories. Journal of Symbolic Computation, 14(5):437–458, November 1992.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next]

[Postscript] [PDF] [BibTeX Source] [LaTeX Source]