Thue trees
type: Item
instance of: scholarly article
title: Thue trees
zbMATH Open document ID: 1020.03039
DOI: 10.1016/S0168-0072(02)00032-5
author: Jerzy Marcinkowski
author: Leszek Pacholski
published in: Annals of Pure and Applied Logic
publication date: 2003-03-09T00:00:00Z
review text: A new technique is introduced to prove undecidability results. This technique is based on the notion of a Thue tree. Also, examples are given how to apply this method to term rewriting, the Horn implication problem, and data dependencies. The strategy of proving undecidability results adapted in this paper is to reduce the problem of existence of a finite Thue tree to the problem under consideration.
Mathematics Subject Classification ID: 03D35
Mathematics Subject Classification ID: 03D03
Mathematics Subject Classification ID: 68Q42
Mathematics Subject Classification ID: 68Q17
Mathematics Subject Classification ID: 68P15
Mathematics Subject Classification ID: 03B35
zbMATH DE Number: 1878501
zbMATH Keywords: undecidability
zbMATH Keywords: Thue systems
zbMATH Keywords: Horn clause implication
zbMATH Keywords: one-step rewriting
MaRDI profile type: Publication
cites work: Solvable cases of the decision problem
cites work: Q3912018
cites work: Q4264713
cites work: Q5691140
cites work: Encompassment properties and automata with constraints
cites work: The Implication Problem for Functional and Inclusion Dependencies is Undecidable
cites work: Q5679729
cites work: More problems in rewriting
cites work: Problems in rewriting III
cites work: Smallest horn clause programs
cites work: Q4281507
cites work: Q4942617
cites work: Q3905252
cites work: The unsolvability of the Gödel class with identity
cites work: Subsumption and implication
cites work: Q3716319
cites work: On the efficiency of subsumption algorithms
cites work: The decision problem for standard classes
cites work: Satisfiability of the smallest binary program
cites work: On the undecidability of implications between embedded multivalued database dependencies
cites work: Q4385543
cites work: The undecidability of the semi-unification problem
cites work: Q4268482
cites work: Q3856727
cites work: The decision problem for formulas with a small number of atomic subformulas
cites work: Q4525287
cites work: Q4230359
cites work: Undecidability of the first order theory of one-step right ground rewriting
cites work: The decision problem for equational bases of algebras
cites work: Undecidable properties of finite sets of equations
cites work: Unsolvable problems for equational theories
cites work: Recursive Unsolvability of a problem of Thue
cites work: Decidability of Second-Order Theories and Automata on Infinite Trees
cites work: Q5573961
cites work: Implication of clauses is undecidable
cites work: Decidability of a portion of the predicate calculus
cites work: The Concept of Weak Substitution in Theorem-Proving
cites work: The first-order theory of one-step rewriting is undecidable
cites work: The first-order theory of one step rewriting in linear noetherian systems is undecidable
cites work: Q5509685
full work available at URL: s0168-0072(02)00032-5
OpenAlex ID: W4212787582
description: scientific article; zbMATH DE number 1878501