Geodesic
Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 16 (1982) no. 4, pp. 331-347.

Voir la notice de l'article provenant de la source Numdam

@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 - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {331--347},
     publisher = {EDP-Sciences},
     volume = {16},
     number = {4},
     year = {1982},
     mrnumber = {707635},
     zbl = {0518.68025},
     language = {en},
     url = {http://geodesic.mathdoc.fr/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 - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY  - 1982
SP  - 331
EP  - 347
VL  - 16
IS  - 4
PB  - EDP-Sciences
UR  - http://geodesic.mathdoc.fr/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 - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 1982
%P 331-347
%V 16
%N 4
%I EDP-Sciences
%U http://geodesic.mathdoc.fr/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 - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 16 (1982) no. 4, pp. 331-347. http://geodesic.mathdoc.fr/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. | Zbl | MR

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

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. | Zbl | MR

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

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. | Zbl | MR

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. | Zbl | MR

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