On Lazy Commutation

1. Arts, T., Giesl, J.: Termination of term rewriting using dependency pairs. Theoretical Computer Science, vol. 236, pp. 133–178 (2000)

   Google Scholar 

2. Bachmair, L., Dershowitz, N.: Commutation, transformation, and termination. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 5–20. Springer, Heidelberg (1986), http://www.cs.tau.ac.il/~nachum/papers/CommutationTermination.pdf

   Chapter  Google Scholar 

3. Blanqui, F., Jouannaud, J.-P., Rubio, A.: HORPO with computability closure: A reconstruction. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS, vol. 4790, pp. 138–150. Springer, Heidelberg (2007)

   Chapter  Google Scholar 

4. Blass, A., Gurevich, Y.: Program termination and well partial orderings. ACM Transactions on Computational Logic (TOCL) 9(3), Article No. 18 (June 2008), http://research.microsoft.com/en-us/um/people/gurevich/opera/178.pdf

5. Di Cosmo, R., Piperno, A.: Expanding extensional polymorphism. In: Dezani-Ciancaglini, M., Plotkin, G.D. (eds.) TLCA 1995. LNCS, vol. 902, pp. 139–153. Springer, Heidelberg (1995)

   Chapter  Google Scholar 

6. Dawson, J.E., Gore, R.: Termination of abstract reduction systems. In: Proceedings of Computing: The Australasian Theory Symposium (CATS 2007), Ballarat, Australia, pp. 35–43 (2007)

   Google Scholar 

7. Dershowitz, N.: Termination of linear rewriting systems (Preliminary version). In: Even, S., Kariv, O. (eds.) ICALP 1981. LNCS, vol. 115, pp. 448–458. Springer, Heidelberg (1981), http://www.cs.tau.ac.il/~nachum/papers/Linear.pdf

   Chapter  Google Scholar 

8. Dershowitz, N.: Orderings for term-rewriting systems. Theoretical Computer Science 17(3), 279–301 (1982)

   Article  MathSciNet  MATH  Google Scholar 

9. Dershowitz, N.: Termination of rewriting. J. of Symbolic Computation 3, 69–116 (1987)

   Article  MathSciNet  MATH  Google Scholar 

10. Dershowitz, N.: Termination by abstraction. In: Demoen, B., Lifschitz, V. (eds.) ICLP 2004. LNCS, vol. 3132, pp. 1–18. Springer, Heidelberg (2004), http://www.cs.tau.ac.il/~nachum/papers/TerminationByAbstraction.pdf

    Chapter  Google Scholar 

11. Dershowitz, N., Hoot, C.: Natural termination. Theoretical Computer Science 142(2), 179–207 (1995)

    Article  MathSciNet  MATH  Google Scholar 

12. Dershowitz, N., Manna, Z.: Proving termination with multiset orderings. Communications of the ACM 22(8), 465–476 (1979)

    Article  MathSciNet  MATH  Google Scholar 

13. Doornbos, H., Backhouse, R., van der Woude, J.: A calculational approach to mathematical induction. Theoretical Computer Science 179, 103–135 (1997)

    Article  MathSciNet  MATH  Google Scholar 

14. Doornbos, H., von Karger, B.: On the union of well-founded relations. Logic Journal of the IGPL 6(2), 195–201 (1998)

    Article  MathSciNet  MATH  Google Scholar 

15. Fernández, M., Jouannaud, J.-P.: Modular termination of term rewriting systems revisited. In: Astesiano, E., Reggio, G., Tarlecki, A. (eds.) Recent Trends in Data Type Specification. LNCS, vol. 906, pp. 255–272. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

16. Ferreira, M.C.F., Zantema, H.: Well-foundedness of term orderings. In: Dershowitz, N. (ed.) CTRS 1994. LNCS, vol. 968, pp. 106–123. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

17. Geser, A.: Relative Termination, Ph.D. dissertation, Fakultät für Mathematik und Informatik, Universität Passau, Germany (1990); also available as: Report 91-03, Ulmer Informatik-Berichte, Universität Ulm (1991), http://ginevras.pil.fbeit.htwk-leipzig.de/pil-website/public_html/geser/diss_geser.ps.gz .

18. Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. J. of the Association for Computing Machinery 27(4), 797–821 (1980)

    Article  MathSciNet  MATH  Google Scholar 

19. Goubault-Larrecq, J.: Well-founded recursive relations. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 484–497. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

20. Hindley, J.R.: The Church-Rosser Property and a Result in Combinatory Logic, Ph.D. thesis, University of Newcastle upon Tyne (1964)

    Google Scholar 

21. Jouannaud, J.-P., Rubio, A.: Higher-order recursive path orderings. In: Proceedings 14th Annual IEEE Symposium on Logic in Computer Science (LICS), Trento, Italy, pp. 402–411 (1999)

    Google Scholar 

22. Kamin, S., Lévy, J.-J.: Attempts for generalising the recursive path orderings, unpublished note, Department of Computer Science, University of Illinois, Urbana, IL (February 1980), http://pauillac.inria.fr/~levy/pubs/80kamin.pdf

23. Klop, J.W.: Combinatory Reduction Systems, Mathematical Centre Tracts 127, CWI, Amsterdam, The Netherlands (1980)

    Google Scholar 

24. Lescanne, P.: On the recursive decomposition ordering with lexicographical status and other related orderings. J. Automated Reasoning 6(1), 39–49 (1990)

    Article  MathSciNet  MATH  Google Scholar 

25. Melliès, P.-A.: On a duality between Kruskal and Dershowitz theorems. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 518–529. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

26. Nash-Williams, C.St.J.A.: On well-quasi-ordering finite trees. Proceedings Cambridge Phil. Soc. 59, 833–835 (1963)

    Article  MathSciNet  MATH  Google Scholar 

27. Newman, M.H.A.: On theories with a combinatorial definition of “equivalence”. Annals of Mathematics 43(2), 223–243 (1942)

    Article  MathSciNet  MATH  Google Scholar 

28. Plaisted, D.A.: Semantic confluence tests and completion methods. Information and Control 65(2/3), 182–215 (1985)

    Article  MathSciNet  MATH  Google Scholar 

29. Porat, S., Francez, N.: Full-commutation and fair-termination in equational (and combined) term-rewriting systems. In: Siekmann, J.H. (ed.) CADE 1986. LNCS, vol. 230, pp. 21–41. Springer, Heidelberg (1986)

    Chapter  Google Scholar 

30. Staples, J.: Church-Rosser theorems for replacement systems. In: Crosley, J. (ed.) Algebra and Logic. Lecture Notes in Mathematics, vol. 450, pp. 291–307. Springer, Heidelberg (1975)

    Chapter  Google Scholar 

31. Struth, G.: Reasoning automatically about termination and refinement (Abstract). In: International Workshop on First-Order Theorem Proving (FTP 2007), Liverpool, UK (September 2007). Full Version at: http://www.dcs.shef.ac.uk/intranet/research/resmes/CS0710.pdf

32. Struth, G.: Personal communication (November 2007)

    Google Scholar 

33. “Terese” (Bezem, M., Klop, J.W., de Vrijer, R., eds.): Term Rewriting Systems. Cambridge University Press, Cambridge (2002)

    Google Scholar 

Download references