A new method for undecidability proofs of first order theories

DOI10.1016/0747-7171(92)90016-WzbMATH Open0769.03026OpenAlexW2011437767MaRDI QIDQ1209623FDOQ1209623

Authors: Ralf Treinen 

Publication date: 16 May 1993

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0747-7171(92)90016-w

Recommendations

• scientific article
• The first-order theory of one-step rewriting is undecidable
• The first-order theory of lexicographic path orderings is undecidable
• Undecidability of the first order theory of one-step right ground rewriting
• The first-order theory of linear one-step rewriting is undecidable

zbMATH Keywords

decision problemterm algebraPost's Correspondence Problempartial lexicographic path orderingundecidability of first order theories

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Undecidability and degrees of sets of sentences (03D35)

Cites Work

• Undecidable theories
• Title not available (Why is that?)
• A variant of a recursively unsolvable problem
• Orderings for term-rewriting systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Fundamental properties of infinite trees
• Termination of rewriting
• Title not available (Why is that?)
• A Unification Algorithm for Associative-Commutative Functions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Concatenation as a basis for arithmetic
• Equational problems and disunification
• Title not available (Why is that?)
• Associative-commutative unification
• Unification theory
• Title not available (Why is that?)
• Title not available (Why is that?)
• SOLVING SYMBOLIC ORDERING CONSTRAINTS
• Title not available (Why is that?)
• Title not available (Why is that?)
• On equational theories, unification, and (un)decidability

Cited In (19)

• Theories of orders on the set of words
• Combination techniques and decision problems for disunification
• Title not available (Why is that?)
• The \(\exists^*\forall^*\) part of the theory of ground term algebra modulo an AC symbol is undecidable.
• Anti-patterns for rule-based languages
• The first-order theory of lexicographic path orderings is undecidable
• The first-order theory of linear one-step rewriting is undecidable
• \(\Sigma_ 1^ 1\)-completeness of a fragment of the theory of trees with subtree relation
• More problems in rewriting
• On equality up-to constraints over finite trees, context unification, and one-step rewriting
• Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq
• Solving simplification ordering constraints
• Thue trees
• Feature automata and recognizable sets of feature trees
• Title not available (Why is that?)
• On the logic of reducibility: Axioms and examples
• Combination techniques and decision problems for disunification
• Problems in rewriting III
• The first-order theory of one-step rewriting is undecidable

This page was built for publication: A new method for undecidability proofs of first order theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1209623)