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.

• Type: Conference
• Year: 2009
• Where: RTA
• Authors: Aleksy Schubert
• Keywords: Formulae, One-step Rewriting Reduction, RTA 2009, Theoretical Computer Science, first-order Theory