A Semi-Thue system is a tuple where
A Semi-Thue system induces a one-step rewrite relation on , which formalises the notion of rewriting a string by replacing a substring within it:
A derivation in the Semi-Thue system is then a (finite or infinite) sequence of words produced by starting with an initial word and repeatedly rewriting it by making one substring-replacement at a time:
If the relation is symmetric, i.e., , then the system is called a Thue system.
A Semi-Thue system is a special type of Post canonical system. A semi-Thue system is also a term-rewriting system — one that has monadic words ending in the same variable as left- and right-hand side terms, e.g. a term rule is equivalent with the string rule .
Semi-Thue systems were developed as part of a program to add additional constructs to logic, so as to create systems such as propositional logic, that would allow general mathematical theorems to be expressed in a formal language, and then proven and verified in an automatic, mechanical fashion. The hope was that the act of theorem proving could then be reduced to a set of defined manipulations on a set of strings. It was subsequently realized that semi-Thue systems are isomorphic to unrestricted grammars, which in turn are known to be isomorphic to Turing machines. And although this program of research succeeded in that computers can now be used to verify the proofs of theorems, it also failed in a spectacular way: a computer cannot distinguish between an interesting theorem, and a boring one.
At the suggestion of Alonzo Church, Emil Post in a paper published in 1947, first proved "a certain Problem of Thue" to be unsolvable, what Martin Davis states as "...the first unsolvability proof for a problem from classical mathematics -- in this case the word problem for semigroups." (Undecidable p. 292)
Davis [ibid] asserts that the proof was offered independently by A. A. Markov (C. R. (Doklady) Acad. Sci. U.S.S.R. (n.s.) 55(1947), pp. 583-586.
The word problem for Semi-Thue systems can be stated as follows: Given a Semi-Thue system and two words , can be transformed into by applying rules from ? This problem is undecidable, i.e. there is no general algorithm for solving this problem. This even holds if we limit the input to finite systems.
Martin Davis offers the lay reader a two-page proof in his article "What is a Computation?" pp. 258-259 with commentary p. 257. Davis casts the proof in this manner: "invent [a word problem] whose solution would lead to a solution to the halting problem."