Sciweavers

RTA
2009
Springer

The Existential Fragment of the One-Step Parallel Rewriting Theory

14 years 5 months ago
The Existential Fragment of the One-Step Parallel Rewriting Theory
It is known that the first-order theory with a single predicate → that denotes one-step rewriting reduction on terms is undecidable already for formulae with ∃∀ prefix. Several decidability results exist for the fragment of the theory in which the formulae start with the ∃ prefix only. This paper considers a similar fragment for a predicate →p which denotes the parallel one-step rewriting reduction. We show that the theory is related to the type entailment problem and prove that the first-order theory of →p is undecidable already for formulae with ∃ prefix.
Aleksy Schubert
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where RTA
Authors Aleksy Schubert
Comments (0)