An algorithm for finding a minimal recursive path ordering
RAIRO. Informatique théorique, Tome 19 (1985) no. 4, pp. 359-382. 
@article{ITA_1985__19_4_359_0,
     author = {A{\"\i}t-Kaci, Hassan},
     title = {An algorithm for finding a minimal recursive path ordering},
     journal = {RAIRO. Informatique th\'eorique},
     pages = {359--382},
     publisher = {EDP-Sciences},
     volume = {19},
     number = {4},
     year = {1985},
     mrnumber = {827483},
     zbl = {0578.68029},
     language = {en},
     url = {http://www.numdam.org/item/ITA_1985__19_4_359_0/}
}
TY  - JOUR
AU  - Aït-Kaci, Hassan
TI  - An algorithm for finding a minimal recursive path ordering
JO  - RAIRO. Informatique théorique
PY  - 1985
SP  - 359
EP  - 382
VL  - 19
IS  - 4
PB  - EDP-Sciences
UR  - http://www.numdam.org/item/ITA_1985__19_4_359_0/
LA  - en
ID  - ITA_1985__19_4_359_0
ER  - 
%0 Journal Article
%A Aït-Kaci, Hassan
%T An algorithm for finding a minimal recursive path ordering
%J RAIRO. Informatique théorique
%D 1985
%P 359-382
%V 19
%N 4
%I EDP-Sciences
%U http://www.numdam.org/item/ITA_1985__19_4_359_0/
%G en
%F ITA_1985__19_4_359_0
Aït-Kaci, Hassan. An algorithm for finding a minimal recursive path ordering. RAIRO. Informatique théorique, Tome 19 (1985) no. 4, pp. 359-382. http://www.numdam.org/item/ITA_1985__19_4_359_0/

[ADJ78] J. A. Goguen, J. W. Thatcher and E. G. Wagner, An Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types, Current Trends in Programming Methodology, in R. T. YEH Ed., V. 4, Prentice Hall, 1978.

[DER 82] (a) N. Dershowitz, Orderings for Term-Rewriting Systems, Theor. Comp. Sc., Vol. 17, (3), pp. 279-301; | MR | Zbl

(b) N. Dershowitz, Computing with Rewrite Systems, Technical Paper Draft, Bar-Ilan University, August 1982.

[DRM79] N. Dershowitz and Z. Manna, Proving Termination with Multiset Ordering, Communications of the A.C.M., Vol. 22, (8), 1979, pp. 465-476. | MR | Zbl

[GOT79] J. A. Goguen and J. J. Tardo, An Introduction to OBJ: a Language for Writing and Testing Formal Algebraic Program Specifications, Proceedings of the I.E.E.E. Conference on Specifications of Reliable Software, Cambridge, MA, 1979, pp. 170-189.

[GOR65] S. Gorn, Explicit Definitions and linguistic Dominoes, in Systems and Computer Science, J. HART, S. TAKASU Eds., University of Toronto Press, 1965. | MR

[HOD82] C. M. Hoffman and M. O'Donnell, Programming with Equations, A.C.M. Transactions on Programming Languages and Systems, Vol. 4, (1), 1982, pp. 83-112. | Zbl

[HOP80] G. Huet and D. C. Oppen, Equations and Rewrite Rules, in Formal Language Theory, Perspective and Open Problems, R. BOOK Ed., Academic Press, 1980, pp. 349-393.

[HUE81] G. Huet, A Complete Proof of Correctness of the Knuth-Bendix Algorithm, J.C.S.S., Vol. 23,(1), 1981, pp. 11-21. | MR | Zbl

[JLR83] J. P. Jouannaud, P. Lescanne and F. Reinig, Recursive Decomposition Ordering, in I.F.I.P. Working Conference on Formal Description of Programming Concepts II, D. BJORNER Ed., North-Holland, 1983. | MR | Zbl

[JOL82] J. P. Jouannaud and P. Lescanne, On Multiset Ordering, Inf. Proc. Lett., Vol. 15, (2), 1982. | MR | Zbl

[LES82] P. Lescanne, Some Properties of Decomposition Path Ordering, a Simplification Ordering to Prove Termination of Rewriting Systems, R.A.I.R.O., Informatique Theorique, Vol. 16, 1982, pp. 331-347. | Numdam | MR | Zbl

[LES83] (a) P. Lescanne, How to Prove Termination? An Approach to the Implementation of a New Recursive Decomposition Ordering, Technical Report, Centre de Recherche en Informatique de Nancy, Nancy, France, July 1983;

(b) P. Lescanne, Computer Experiments with the REVE Rewriting System Generator, in Proceedings of the 10th POPL Symposium, 1983.

[KNB70] D. E. Knuth and P. Bendix, Simple Word Problems in Universal Algebra, in Computational Problems in Abstract Algebra, J. LEECH Ed., Pergamon Press, 1970, pp. 263-297. | MR | Zbl

[MUS79] D. R. Musser, Abstract Data Types Specification in the AFFIRM System, Proceedings of the I.E.E.E. Conference on Specifications of Reliable Software, Cambridge, Ma., 1979, pp. 45-57.

[ODN78] M. O'Donnell, Computing in Systems Described by Equations, Lecture Notes in Computer Science, Vol. 58, Springer-Verlag, 1978. | MR | Zbl

[PLT78] D. Plaisted, A Recursively Defined Ordering for Proving Termination of Term-Rewriting Systems, Report R-78-943, Department of Computer Science, University of Illinois, Urbana, III., 1978.

[PTS81] G. E. Peterson and M. E. Stickel, Complete Sets of Reductions for some Equational Theories, J.A.C.M., Vol. 28, (2), 1981, pp. 233-264. | MR | Zbl

[ROS73] B. K. Rosen, Tree-Manipulating Systems and Church-Rosser Theorems, J.A.C.M., Vol. 20, (1), 1973, pp. 160-187. | MR | Zbl