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. This method of research succeeded and now computers can be used to verify the proofs of mathematic and logical theorems. 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." Davis also asserts that the proof was offered independently by A. A. Markov. See also L-system MU puzzle Notes References Monographs Ronald V. Book and Friedrich Otto, String-rewriting Systems, Springer, 1993, . Matthias Jantzen, Confluent string rewriting, Birkhäuser, 1988, . Textbooks Martin Davis, Ron Sigal, Elaine J. Weyuker, Computability, complexity, and languages: fundamentals of theoretical computer science, 2nd ed., Academic Press, 1994, , chapter 7 Elaine Rich, Automata, computability and complexity: theory and applications, Prentice Hall, 2007, , chapter 23.5. Surveys Samson Abramsky, Dov M. Gabbay, Thomas S. E. Maibaum (ed.), Handbook of Logic in Computer Science: Semantic modelling, Oxford University Press, 1995, . Grzegorz Rozenberg, Arto Salomaa (ed.), Handbook of Formal Languages: Word, language, grammar, Springer, 1997, . Landmark papers Formal languages Theory of computation Rewriting systems ja:文字列書き換え系