[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #93

Originator: Ralf Treinen [Tre96]
Date: 1996

Summary: Are the existential fragment or the positive fragment of the theory of one-step rewriting decidable?

For a given signature Σ and rewrite system R, the theory of one-step rewriting by R is the first order theory of the model comprising all Σ-ground-terms, and the binary predicate x rewrites to y in one rewrite step of R.

It is well-known that the full first-order theory is undecidable, even for strong restrictions on the class of rewrite systems (see Problem #51). Is the existential fragment of this theory (in other words: satisfiability of quantifier-free formulas) decidable? Is the positive fragment (arbitrary quantification, but no negation or implications) decidable?

It is known that the positive existential fragment is decidable [NPR97], and there are decidability results for the full existential fragment in case of restricted classes of rewrite systems [CSTT99, LR99].

References

[CSTT99]
Anne-Cécile Caron, Franck Seynhaeve, Sophie Tison, and Marc Tommasi. Deciding the satisfiability of quantifier free formulae on one-step rewriting. In Narendran and Rusinowitch [NR99], pages 103–117.
[LR99]
Sébastien Limet and Pierre Réty. A new result about the decidability of the existential one-step rewriting theory. In Narendran and Rusinowitch [NR99], pages 118–132.
[NPR97]
Joachim Niehren, Manfred Pinkal, and Peter Ruhrberg. On equality up-to constraints over finite trees, context unification and one-step rewriting. In William McClune, editor, 14th International Conference on Automated Deduction, volume 1249 of Lecture Notes in Artificial Intelligence, pages 34–48, Townsville, Australia, July 1997. Springer-Verlag.
[NR99]
Paliath Narendran and Michael Rusinowitch, editors. 10th International Conference on Rewriting Techniques and Applications, volume 1631 of Lecture Notes in Computer Science, Trento, Italy, July 1999. Springer-Verlag.
[Tre96]
Ralf Treinen. The first-order theory of one-step rewriting is undecidable. In Harald Ganzinger, editor, 7th International Conference on Rewriting Techniques and Applications, volume 1103 of Lecture Notes in Computer Science, pages 276–286, New Brunswick, NJ, USA, July 1996. Springer-Verlag.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]