The first-order theory of linear one-step rewriting is undecidable

DOI10.1016/S0304-3975(98)00083-8zbMath0912.68102MaRDI QIDQ1275021

Ralf Treinen

Publication date: 12 January 1999

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

term-rewriting system

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

First-order theory of rewriting for linear variable-separated rewrite systems: automation, formalization, certification ⋮ Proving semantic properties as first-order satisfiability ⋮ Unnamed Item ⋮ The Existential Fragment of the One-Step Parallel Rewriting Theory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Decidability of unification in the theory of one-sided distributivity and a multiplicative unit
• A new method for undecidability proofs of first order theories
• Semantic confluence tests and completion methods
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Semantics-Based Translation Methods for Modal Logics
• Undecidability of the first order theory of one-step right ground rewriting
• The first-order theory of one step rewriting in linear noetherian systems is undecidable
• Encompassment properties and automata with constraints
• More problems in rewriting
• Problems in rewriting III
• The first-order theory of one-step rewriting is undecidable
• On equality up-to constraints over finite trees, context unification, and one-step rewriting
• A variant of a recursively unsolvable problem