Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems
RAIRO. Informatique théorique, Tome 16 (1982) no. 4, pp. 331-347. 
@article{ITA_1982__16_4_331_0,
     author = {Lescanne, Pierre},
     title = {Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems},
     journal = {RAIRO. Informatique th\'eorique},
     pages = {331--347},
     publisher = {EDP-Sciences},
     volume = {16},
     number = {4},
     year = {1982},
     mrnumber = {707635},
     zbl = {0518.68025},
     language = {en},
     url = {http://www.numdam.org/item/ITA_1982__16_4_331_0/}
}
TY  - JOUR
AU  - Lescanne, Pierre
TI  - Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems
JO  - RAIRO. Informatique théorique
PY  - 1982
SP  - 331
EP  - 347
VL  - 16
IS  - 4
PB  - EDP-Sciences
UR  - http://www.numdam.org/item/ITA_1982__16_4_331_0/
LA  - en
ID  - ITA_1982__16_4_331_0
ER  - 
%0 Journal Article
%A Lescanne, Pierre
%T Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems
%J RAIRO. Informatique théorique
%D 1982
%P 331-347
%V 16
%N 4
%I EDP-Sciences
%U http://www.numdam.org/item/ITA_1982__16_4_331_0/
%G en
%F ITA_1982__16_4_331_0
Lescanne, Pierre. Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems. RAIRO. Informatique théorique, Tome 16 (1982) no. 4, pp. 331-347. http://www.numdam.org/item/ITA_1982__16_4_331_0/

1. N. Dershowitz, Ordering for Term Rewriting Systems, Proc. 20th Symposium on Foundations of Computer Science, 1979, pp. 123-131, also in Theoritical Computer Science, Vol. 17, 1982, pp. 279-301. | MR | Zbl

2. N. Dershowitz, A note on Simplification Orderings, Inform. Proc. Ltrs., Vol. 9, 1979, pp. 212-215. | MR | Zbl

3. J. Françon, G. Viennot and J. Vuillemin, Description and Analysis of an Efficient Priority Queues Representation, Proc. 19th Symposium of Foundations of Computer Science, 1978, pp. 1-7. | MR

4. G. Huet, A Complete Proof of Correctness of the Knuth-Bendix Completion Algorithm, Rapport INRIA 25, 1980. | MR

5. G. Huet and J. Hullot, Proof by Induction in Equational Theories with Constructors, Proc. 21th Symposium on Foundations of Computer Science, 1980.

6. G. Huet and D. C. Oppen, Equations and Rewrite Rules: a Survey, in Formal Languages perspectives and Open Problems, R. BOOK, Ed., Academic Press, 1980.

7. D. E. Knuth, The Art of Computer Programming. Vol. 1: Fundamental Algorithms, Addison Wesley, Reading, Mass., 1968. | MR

8. 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

9. J. B. Kruskal, Well-Quasi-Ordering, the Tree Theorem, and Vazsonyi's Conjecture, Trans. Amer. Math. Soc., Vol. 95, 1960, pp. 210-225. | MR | Zbl

10. P. Lescanne, Two Implementations of the Recursive Path Ordering on Monadic Terms, 19th Annual Allerton Conf. on Communication, Control, and Computing, Allerton House, Monticello, Illinois, 1981.

11. P. Lescanne, Decomposition Ordering as a Tool to prove the Termination of Rewriting Systems, 7th IJCAI, Vancouver, Canada, 1981, pp. 548-550.

12. P. Lescanne and F. Reinig, A Well-Founded Recursively Defined Ordering on First Order Terms, Centre de Recherche en Informatique de Nancy, France, CRIN 80-R-005.

13. D. L. Musser, On Proving Inductive Properties of Abstract Data Types, Proc. 7th ACM Symposium on Principles of Programming Languages, 1980.

14. C. St. J. A. Nash-William, On Well-Quasi-Ordering on Finite Trees, Proc. Cambridge Philos. Soc., Vol. 60, 1964, pp. 833-835. | MR | Zbl

15. D. Plaisted, Well-Founded Orderings for Proving Termination of Systems of Rewrite Rules, Dept of Computer Science Report 78-932, U. of Illinois at Urbana-Champaign, July 1978.

16. D. Plaisted, A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems, Dept of Computer Science Report 78-943, U. of Illinois at Urbana-Champaign, Sept. 1978.

17. F. Reinig, Les ordres de décomposition: un outil incrémental pour prouver la terminaison finie de systèmes de réécriture de termes, Thèse, Université de Nancy, 1981.

18. J.-P. Jouannaud and P. Lescanne, On Multiset Orderings, in Inform. Proc. Ltrs., Vol. 15, 1982, pp. 57-63. | MR | Zbl

19. J.-P. Jouannaud, P. Lescanne and F. Reinig, Recursive Decomposition Ordering, IFIP Conf. on Formal Description of Programming Concepts, Garmisch-Partenkirchen, Germany, 1982. | MR | Zbl