Some properties of decomposition ordering, a simplification ordering to prove termination of rewriting systems
Lescanne, Pierre
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 16 (1982), p. 331-347 / Harvested from Numdam
Access to full text
Full (PDF)
Full (DJVU) 
@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},
     volume = {16},
     year = {1982},
     pages = {331-347},
     mrnumber = {707635},
     zbl = {0518.68025},
     language = {en},
     url = {http://dml.mathdoc.fr/item/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) pp. 331-347. http://gdmltest.u-ga.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. | MR 648438 | Zbl 0525.68054

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

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 539825

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

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 378456

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 255472 | Zbl 0188.04902

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 111704 | Zbl 0158.27002

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 153601 | Zbl 0122.25001

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 675869 | Zbl 0486.68041

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 787625 | Zbl 0513.68026