An algorithm for finding a minimal recursive path ordering

 Access to full text

 Full (PDF)

1. [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. 
2. [DER 82] (a) N. DERSHOWITZ, Orderings for Term-Rewriting Systems, Theor. Comp. Sc., Vol. 17, (3), pp. 279-301; Zbl0525.68054MR648438
3. (b) N. DERSHOWITZ, Computing with Rewrite Systems, Technical Paper Draft, Bar-Ilan University, August 1982. 
4. [DRM79] N. DERSHOWITZ and Z. MANNA, Proving Termination with Multiset Ordering, Communications of the A.C.M., Vol. 22, (8), 1979, pp. 465-476. Zbl0431.68016MR540043
5. [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. 
6. [GOR65] S. GORN, Explicit Definitions and linguistic Dominoes, in Systems and Computer Science, J. HART, S. TAKASU Eds., University of Toronto Press, 1965. MR237245
7. [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. Zbl0481.68008
8. [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. 
9. [HUE81] G. HUET, A Complete Proof of Correctness of the Knuth-Bendix Algorithm, J.C.S.S., Vol. 23,(1), 1981, pp. 11-21. Zbl0465.68014MR636177
10. [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. Zbl0513.68026MR787625
11. [JOL82] J. P. JOUANNAUD and P. LESCANNE, On Multiset Ordering, Inf. Proc. Lett., Vol. 15, (2), 1982. Zbl0486.68041MR675869
12. [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. Zbl0518.68025MR707635
13. [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; 
14. (b) P. LESCANNE, Computer Experiments with the REVE Rewriting System Generator, in Proceedings of the 10th POPL Symposium, 1983. 
15. [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. Zbl0188.04902MR255472
16. [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. 
17. [ODN78] M. O'DONNELL, Computing in Systems Described by Equations, Lecture Notes in Computer Science, Vol. 58, Springer-Verlag, 1978. Zbl0421.68038MR483644
18. [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. 
19. [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. Zbl0479.68092MR612079
20. [ROS73] B. K. ROSEN, Tree-Manipulating Systems and Church-Rosser Theorems, J.A.C.M., Vol. 20, (1), 1973, pp. 160-187. Zbl0267.68013MR331850