A new method for undecidability proofs of first order theories

DOI10.1016/0747-7171(92)90016-WMaRDI QIDQ1209623zbMATH OpenOpenAlexFDO

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

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)

Recommendations

• scientific article; zbMATH DE number 4210102
• 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

Cites work

• scientific article; zbMATH DE number 3888893 (Why is no real title available?)
• scientific article; zbMATH DE number 3950473 (Why is no real title available?)
• scientific article; zbMATH DE number 3976991 (Why is no real title available?)
• scientific article; zbMATH DE number 176755 (Why is no real title available?)
• scientific article; zbMATH DE number 3467028 (Why is no real title available?)
• scientific article; zbMATH DE number 1348479 (Why is no real title available?)
• scientific article; zbMATH DE number 1142313 (Why is no real title available?)
• scientific article; zbMATH DE number 1142316 (Why is no real title available?)
• scientific article; zbMATH DE number 3291134 (Why is no real title available?)
• scientific article; zbMATH DE number 3304995 (Why is no real title available?)
• scientific article; zbMATH DE number 3336816 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• A Unification Algorithm for Associative-Commutative Functions
• A variant of a recursively unsolvable problem
• Associative-commutative unification
• Concatenation as a basis for arithmetic
• Equational problems and disunification
• Fundamental properties of infinite trees
• On equational theories, unification, and (un)decidability
• Orderings for term-rewriting systems
• SOLVING SYMBOLIC ORDERING CONSTRAINTS
• Termination of rewriting
• Undecidable theories
• Unification theory

Cited in

(19)

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