The Tyrolean Termination Tool 2 (TTT2) is a tool for automatically proving (and disproving) termination of term rewrite systems. It is the completely redesigned successor of TTT. Current (non-)termination techniques include: approximated dependency graph, argument filtering, bounds, dependency pair method, Knuth-Bendix order, lexicographic path order, loop detection, matrix interpretation, polynomial interpretation, predictive labeling, recursive SCC, root-labeling, semantic labeling, simple projection and subterm criterion, uncurrying, and usable rules.

References in zbMATH (referenced in 66 articles )

Showing results 1 to 20 of 66.
Sorted by year (citations)

1 2 3 4 next

  1. Felgenhauer, Bertram; Thiemann, René: Reachability, confluence, and termination analysis with state-compatible automata (2017)
  2. Iborra, José; Nishida, Naoki; Vidal, Germán; Yamada, Akihisa: Relative termination via dependency pairs (2017)
  3. Lucas, Salvador; Meseguer, José: Dependency pairs for proving termination properties of conditional term rewriting systems (2017)
  4. Moser, Georg: KBOs, ordinals, subrecursive hierarchies and all that (2017)
  5. Sabel, David; Zantema, Hans: Termination of cycle rewriting by transformation and matrix interpretation (2017)
  6. Avanzini, Martin; Moser, Georg: A combination framework for complexity (2016)
  7. Iborra, José; Nishida, Naoki; Vidal, Germán; Yamada, Akihisa: Reducing relative termination to dependency pair problems (2015)
  8. Zankl, Harald; Winkler, Sarah; Middeldorp, Aart: Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations (2015)
  9. Kordy, Barbara; Mauw, Sjouke; Radomirović, Saša; Schweitzer, Patrick: Attack-defense trees (2014)
  10. Neurauter, Friedrich; Middeldorp, Aart: Polynomial interpretations over the natural, rational and real numbers revisited (2014)
  11. Zankl, Harald; Korp, Martin: Modular complexity analysis for term rewriting (2014)
  12. Aoto, Takahito: Disproving confluence of term rewriting systems by interpretation and ordering (2013)
  13. Bofill, Miquel; Borralleras, Cristina; Rodríguez-Carbonell, Enric; Rubio, Albert: The recursive path and polynomial ordering for first-order and higher-order terms (2013)
  14. Hirokawa, Nao; Middeldorp, Aart; Zankl, Harald: Uncurrying for termination and complexity (2013)
  15. Winkler, Sarah; Sato, Haruhiko; Middeldorp, Aart; Kurihara, Masahito: Multi-completion with termination tools (2013)
  16. Bouhoula, Adel; Jacquemard, Florent: Sufficient completeness verification for conditional and constrained TRS (2012)
  17. Codish, Michael; Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René: SAT solving for termination proofs with recursive path orders and dependency pairs (2012)
  18. Kop, Cynthia; van Raamsdonk, Femke: Dynamic dependency pairs for algebraic functional systems (2012)
  19. Sternagel, Thomas; Zankl, Harald: KBCV -- Knuth-Bendix completion visualizer (2012)
  20. Fuhs, Carsten; Giesl, Jürgen; Parting, Michael; Schneider-Kamp, Peter; Swiderski, Stephan: Proving termination by dependency pairs and inductive theorem proving (2011)

1 2 3 4 next