 On
the termination of Markov algorithms Zohar Manna and
Steven Ness, Proc. of the Third Hawaii International
Conference on System Science, Honolulu, HI, pp. 789792
(January 1970)
Despite its name, it is a paper on termination of term rewriting systems, the second (after Saul Gorn's paper. (1967), Handling the growth
by definition of mechanical languages, Proceedings of
the AFIPS 1967 Spring Joint Computer Conference,
Philadelphia, PA, Vol. 30, AFIPS Press, pages 213224, thanks to Nachum Dershowitz for the reference) proposing a
method for proving termination of term rewrite systems,
actually a method based on linear function (i. e.,
polynomial of degree 1).
 On
the Uniform Halting Problem for Term Rewriting Systems
Gerard Huet and Dallas Lankford (March 1978) Rapport
IRIA Laboria N° 283, Rocquencourt, France.
The reference for the undecidability of the termination
of Term Rewriting Systems and the decidability of the
termination of Ground Term Rewriting Systems.
 Wellfounded
Orderings for Proving Termination of Term Rewriting
Systems David Plaisted (July 1978), Dept. of
Computer Science Report, Research Report 78932 University of
Illinois At UrbanaChampaign
An ancestor of the famous recursive path ordering.
 A Recursively Defined
Ordering for Proving Termination of Term Rewriting Systems
by David Plaisted (September 1978), Dept. of Computer
Science Report, Research Report 78943 University of Illinois
At UrbanaChampaign
A sibling of the recursive path ordering.
 On Proving term rewriting
systems are Noetherian by Dallas Lankford (May 1979).
This folk paper presents methods for proving termination of
TRS based on interpretations, especially on polynomial
interpretations.
 Attempts
for generalizing the recursive path orderings by Sam Kamin
and JeanJacques Levy (February 1st 1980).
This folk handwritten paper by Sam Kamin and JeanJacques
Lévy is the first reference to the semantic path ordering and
the lexicographic path ordering

Dershowitzeries
by JeanJacques Levy (Oct 1981).
Those are handwritten lecture notes, in French, of a talk
that JeanJacques Levy gave on October 23 1981 about what is
known now as the semantic path ordering and which he calls
rpo.
 Kruskaleries
by JeanJacques Levy (Oct 1981).
Those are handwritten lecture notes, in French, of a talk
that JeanJacques Levy gave on October 15 1981 about
NashWilliam proof of Kruskal theorem. This paper was the
origin of the following paper: J. Gallier. What's so
special about Kruskal's Theorem and the ordinal Gamma_0 ? A
survey of some results in proof theory. Annals of
Pure and Applied Logic 53 (1991), 199260.
 On Multiset
Orderings, by JeanPierre Jouannaud and Pierrre
Lescanne, preliminary version of a paper published in
Inf. Process. Lett. 15(2) 5763 (1982).
Presentation of a refutation complete method in presence of rewrite rules based on paramodulation.