[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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].
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |