Labelings for Decreasing Diagrams

1. Aoto, T.: Automated confluence proof by decreasing diagrams based on rule-labelling. In: Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics 6, 7–16 (2010)

   MathSciNet  Google Scholar 

2. Aoto, T., Toyama, Y.: A reduction-preserving completion for proving confluence of non-terminating term rewriting systems. Logical Methods in Computer Science 8(1:31), 1–29 (2012)

   MathSciNet  Google Scholar 

3. Aoto, T., Toyama, Y.: Persistency of confluence. Journal of Universal Computer Science 3(11), 1134–1147 (1997)

   MathSciNet  MATH  Google Scholar 

4. Aoto, T., Yoshida, J., Toyama, Y.: Proving confluence of term rewriting systems automatically. In: Proceedings of the 20th International Conference on Rewriting Techniques and Applications. Lect. Notes Comput. Sci. 5595, 93–102 (2009)

   Article  MathSciNet  Google Scholar 

5. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)

6. Felgenhauer, B.: Rule labeling for confluence of left-linear term rewrite systems. In: Proceedings of the 2nd International Workshop on Confluence, pp. 23–27 (2013)

7. Felgenhauer, B., Zankl, H., Middeldorp, A.: Proving confluence with layer systems. In: Proceedings of the 31st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics 13, 288–299 (2011)

   MathSciNet  Google Scholar 

8. Geser, A. Relative termination. Ph.D. thesis, Universität Passau (1990). Available as technical report 91-03

9. Gramlich, B.: Confluence without termination via parallel critical pairs. In: Proceedings of the 21st International Colloquium on Trees in Algebra and Programming. Lect. Notes Comput. Sci. 1059, 211–225 (1996)

   Article  MathSciNet  Google Scholar 

10. Hirokawa, N., Middeldorp, A.: Commutation via relative termination. In: Proceedings of the 2nd International Workshop on Confluence, pp. 29–33 (2013)

11. Hirokawa, N., Middeldorp, A.: Decreasing diagrams and relative termination. J. Autom. Reason. 47(4), 481–501 (2011)

    Article  MathSciNet  MATH  Google Scholar 

12. Huet, G.: Confluent reductions: Abstract properties and applications to term rewriting systems. J. ACM 27(4), 797–821 (1980)

    Article  MathSciNet  MATH  Google Scholar 

13. Klein, D., Hirokawa, N.: Confluence of non-left-linear TRSs via relative termination. In: Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Lect. Notes Comput. Sci. 7180, 258–273 (2012). (Advanced Research in Computing and Software Science)

    Article  MathSciNet  Google Scholar 

14. Knuth, D., Bendix, P.: Simple word problems in universal algebras. In: Leech, J. (ed.) Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press (1970)

15. Okui, S.: Simultaneous critical pairs and Church-Rosser property. In: Proceedings of the 9th International Conference on Techniques, Rewriting, Applications. Lect. Notes Comput. Sci. 1379, 2–16 (1998)

    Article  MathSciNet  Google Scholar 

16. van Oostrom, V.: Confluence by decreasing diagrams. Theor. Comput. Sci. 126(2), 259–280 (1994)

    Article  MathSciNet  MATH  Google Scholar 

17. van Oostrom, V.: Confluence by decreasing diagrams – converted. In: Proceedings of the 19th International Conference on Rewriting Techniques and Applications. Lecture Notes in Computer Science 5117, 306–320 (2008)

    Article  MathSciNet  Google Scholar 

18. van Oostrom, V.: Confluence via critical valleys. In: Proceedings 6th International Workshop on Higher-Order Rewriting, pp. 9–11 (2012)

19. van Oostrom, V.: Developing developments. Theor. Comput. Sci. 175(1), 159–181 (1997)

    Article  MathSciNet  MATH  Google Scholar 

20. Oyamaguchi, M., Ohta, Y.: A new parallel closed condition for Church-Rosser of left-linear term rewriting systems. In: Proceedings of the 8th International Conference on Rewriting Techniques and Applications. Lect. Notes Comput. Sci. 1232 (1997), 187–201

21. Rosen, B.: Tree-manipulating systems and Church-Rosser theorems. J. ACM 20(1), 160–187 (1973)

    Article  MATH  Google Scholar 

22. Stump, A., Zantema, H., Kimmell, G., Omar, R.: A rewriting view of simple typing. Logical Methods in Computer Science 9(1:4), 1–29 (2012)

    Google Scholar 

23. Terese: Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, vol. 55. Cambridge University Press (2003)

24. Toyama, Y.: Commutativity of term rewriting systems. In: Fuchi, K., Kott, L. (eds.) Programming of Future Generation Computers II, pp. 393–407. North-Holland (1988)

25. Toyama, Y.: On the Church-Rosser property for the direct sum of term rewriting systems. J. ACM 34(1), 128–143 (1987)

    Article  MathSciNet  MATH  Google Scholar 

26. Toyama, Y.: On the Church-Rosser property of term rewriting systems. Tech. Rep. 17672 (1981). NTT ECL

27. Waldmann, U.: Semantics of order-sorted specifications. Theor. Comput. Sci. 94(1), 1–35 (1992)

    Article  MathSciNet  MATH  Google Scholar 

28. Zankl, H.: Confluence by decreasing diagrams – formalized. In: Proceedings of the 24th International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics 21, 352–367 (2013)

    MathSciNet  Google Scholar 

29. Zankl, H. Decreasing diagrams. Archive of Formal Proofs (2013). Formal proof development, http://afp.sf.net/entries/Decreasing-Diagrams.shtml

30. Zankl, H., Felgenhauer, B., Middeldorp, A.: CSI – A confluence tool. In: Proceedings of the 23rd International Conference on Deduction, Automated. Lecture Notes in Artificial Intelligence 6803, 499–505 (2011)

    MathSciNet  Google Scholar 

31. Zankl, H., Felgenhauer, B., Middeldorp, A.: Labelings for decreasing diagrams. In: Proceedings of the 22nd International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics 10, 377–392 (2011)

    MathSciNet  Google Scholar 

Download references