References

  1. Takahito Aoto (2013): Disproving Confluence of Term Rewriting Systems by Interpretation and Ordering. In: Proc. FroCoS, LNCS 8152. Springer, pp. 311–326, doi:10.1007/978-3-642-40885-4_22.
  2. Thomas Arts & Jürgen Giesl (2000): Termination of Term Rewriting using Dependency Pairs. Theoretical Computer Science 236(\voidb@x 1-2), pp. 133–178, doi:10.1016/S0304-3975(99)00207-8.
  3. Martin Avanzini & Georg Moser (2013): Tyrolean Complexity Tool: Features and Usage. In: Proc. RTA, LIPIcs 21. Dagstuhl, pp. 71–80, doi:10.4230/LIPIcs.RTA.2013.71.
  4. Frédéric Blanqui & Adam Koprowski (2011): CoLoR: a Coq library on well-founded rewrite relations and its application on the automated verification of termination certificates. Mathematical Structures in Computer Science 21(4), pp. 827–859, doi:10.1017/S0960129511000120.
  5. Michael Codish, Carsten Fuhs, Jürgen Giesl & Peter Schneider-Kamp (2010): Lazy Abstraction for Size-Change Termination. In: Proc. LPAR, LNCS 6397. Springer, pp. 217–232, doi:10.1007/978-3-642-16242-8_16.
  6. Évelyne Contejean, Pierre Courtieu, Julien Forest, Olivier Pons & Xavier Urbain (2011): Automated Certified Proofs with C-0.1exiME3. In: Proc. RTA, LIPIcs 10. Dagstuhl, pp. 21–30, doi:10.4230/LIPIcs.RTA.2011.21.
  7. Nachum Dershowitz (1987): Termination of Rewriting. Journal of Symbolic Computation 3(\voidb@x 1-2), pp. 69–116, doi:10.1016/S0747-7171(87)80022-6.
  8. Fabian Emmes, Tim Enger & Jürgen Giesl (2012): Proving Non-Looping Non-Termination Automatically. In: Proc. IJCAR, LNCS 7364. Springer, pp. 225–240, doi:10.1007/978-3-642-31365-3_19.
  9. Jörg Endrullis, Johannes Waldmann & Hans Zantema (2008): Matrix Interpretations for Proving Termination of Term Rewriting. Journal of Automated Reasoning 40(\voidb@x 2-3), pp. 195–220, doi:10.1007/s10817-007-9087-9.
  10. Bertram Felgenhauer & René Thiemann (2014): Reachability Analysis with State-Compatible Automata. In: Proc. LATA, LNCS 8370. Springer, pp. 347–359, doi:10.1007/978-3-319-04921-2_28.
  11. Alfons Geser, Dieter Hofbauer, Johannes Waldmann & Hans Zantema (2007): On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems. Information and Computation 205(4), pp. 512–534, doi:10.1007/978-3-540-32033-3_26.
  12. Jürgen Giesl, Marc Brockschmidt, Fabian Emmes, Florian Frohn, Carsten Fuhs, Carsten Otto, Martin Plücker, Peter Schneider-Kamp, Thomas Ströder, Steffi Swiderski & René Thiemann (2014): Proving Termination of Programs Automatically with AProVE. In: Proc. IJCAR, LNAI 8562. Springer, pp. 184–191, doi:10.1007/978-3-319-08587-6_13.
  13. Jürgen Giesl, René Thiemann, Peter Schneider-Kamp & Stephan Falke (2006): Mechanizing and Improving Dependency Pairs. Journal of Automated Reasoning 37(3), pp. 155–203, doi:10.1007/s10817-006-9057-7.
  14. Bernhard Gramlich (1995): Abstract Relations between Restricted Termination and Confluence Properties of Rewrite Systems. Fundamenta Informaticae 24(\voidb@x 1-2), pp. 3–23, doi:10.3233/FI-1995-24121.
  15. Nao Hirokawa & Aart Middeldorp (2007): Tyrolean Termination Tool: Techniques and Features. Information and Computation 205(4), pp. 474–511, doi:10.1016/j.ic.2006.08.010.
  16. Nao Hirokawa, Aart Middeldorp & Harald Zankl (2013): Uncurrying for Termination and Complexity. Journal of Automated Reasoning 50(3), pp. 279–315, doi:10.1007/s10817-012-9248-3.
  17. Donald E. Knuth & Peter B. Bendix (1970): Simple Word Problems in Universal Algebras. In: Computational Problems in Abstract Algebra, pp. 263–297, doi:10.1016/B978-0-08-012975-4.50028-X.
  18. Adam Koprowski & Johannes Waldmann (2008): Arctic Terminationłdots Below Zero. In: Proc. RTA, LNCS 5117. Springer, pp. 202–216, doi:10.1007/978-3-540-70590-1_14.
  19. Martin Korp, Christian Sternagel, Harald Zankl & Aart Middeldorp (2009): Tyrolean Termination Tool 2. In: Proc. RTA, LNCS 5595. Springer, pp. 295–304, doi:10.1007/978-3-642-02348-4_21.
  20. Dallas Lankford (1979): On Proving Term Rewriting Systems are Noetherian. Technical Report MTP-3. Louisiana Technical University, Ruston, LA, USA.
  21. Chin Soon Lee, Neil D. Jones & Amir M. Ben-Amram (2001): The Size-Change Principle for Program Termination. In: Proc. POPL. ACM New York, NY, USA, pp. 81–92, doi:10.1145/373243.360210.
  22. Salvador Lucas (2005): Polynomials over the reals in proofs of termination: From theory to practice. RAIRO – Theoretical Informatics and Applications 39(3), pp. 547–586, doi:10.1051/ita:2005029.
  23. Christian Sternagel & Aart Middeldorp (2008): Root-Labeling. In: Proc. RTA, LNCS 5117. Springer, pp. 336–350, doi:10.1007/978-3-540-70590-1_23.
  24. Christian Sternagel & René Thiemann (2011): Generalized and Formalized Uncurrying. In: Proc. FroCoS, LNAI 6989. Springer, pp. 243–258, doi:10.1007/978-3-642-24364-6_17.
  25. Thomas Sternagel & Harald Zankl (2012): KBCV – Knuth-Bendix Completion Visualizer. In: Proc. IJCAR, LNCS 7364. Springer, pp. 530–536, doi:10.1007/978-3-642-31365-3_41.
  26. René Thiemann & Jürgen Giesl (2005): The size-change principle and dependency pairs for termination of term rewriting. Applicable Algebra in Engineering, Communication and Computing 16(4), pp. 229–270, doi:10.1007/s00200-005-0179-7.
  27. René Thiemann & Christian Sternagel (2009): Certification of Termination Proofs using C-0.2exe-0.5exT-0.5exA. In: Proc. TPHOLs, LNCS 5674. Springer, pp. 452–468, doi:10.1007/978-3-642-03359-9_31.
  28. Xavier Urbain (2001): Automated incremental termination proofs for hierarchically defined term rewriting systems. In: Proc. IJCAR, LNAI 2083. Springer, pp. 485–498, doi:10.1007/3-540-45744-5_42.
  29. Johannes Waldmann (2004): Matchbox: A Tool for Match-Bounded String Rewriting. In: Proc. RTA, LNCS 3091. Springer, pp. 85–94, doi:10.1007/978-3-540-25979-4_6.
  30. Sarah Winkler, Haruhiko Sato, Aart Middeldorp & Masahito Kurihara (2013): Multi-Completion with Termination Tools. Journal of Automated Reasoning 50(3), pp. 317–354, doi:10.1007/s10817-012-9249-2.
  31. Harald Zankl, Bertram Felgenhauer & Aart Middeldorp (2011): CSI – A Confluence Tool. In: Proc. CADE, LNAI 6803. Springer, pp. 499–505, doi:10.1007/978-3-642-22438-6_38.
  32. Harald Zankl & Martin Korp (2014): Modular Complexity Analysis for Term Rewriting. Logical Methods in Computer Science 10(\voidb@x 1:19), pp. 1–33, doi:10.2168/LMCS-10(1:19)2014.
  33. Hans Zantema (1995): Termination of Term Rewriting by Semantic Labelling. Fundamenta Informaticae 24(\voidb@x 1-2), pp. 89–105, doi:10.3233/FI-1995-24124.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org