A new method for undecidability proofs of first order theories

DOI10.1016/0747-7171(92)90016-WzbMath0769.03026OpenAlexW2011437767MaRDI QIDQ1209623

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

zbMATH Keywords

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

Mathematics Subject Classification ID

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

Related Items (14)

Feature automata and recognizable sets of feature trees ⋮ \(\Sigma_ 1^ 1\)-completeness of a fragment of the theory of trees with subtree relation ⋮ More problems in rewriting ⋮ Problems in rewriting III ⋮ The first-order theory of one-step rewriting is undecidable ⋮ Solving simplification ordering constraints ⋮ The first-order theory of lexicographic path orderings is undecidable ⋮ The \(\exists^*\forall^*\) part of the theory of ground term algebra modulo an AC symbol is undecidable. ⋮ Combination techniques and decision problems for disunification ⋮ Anti-patterns for rule-based languages ⋮ Combination techniques and decision problems for disunification ⋮ Theories of orders on the set of words ⋮ The first-order theory of linear one-step rewriting is undecidable ⋮ On equality up-to constraints over finite trees, context unification, and one-step rewriting

Cites Work

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

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