A new method for undecidability proofs of first order theories

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

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)

Cites Work

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

Cited In (17)

• Theories of orders on the set of words
• Combination techniques and decision problems for disunification
• 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
• 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)