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 89 articles )

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

1 2 3 4 5 next

  1. Lucas, Salvador: Using well-founded relations for proving operational termination (2020)
  2. Hirokawa, Nao; Nagele, Julian; Middeldorp, Aart: Cops and CoCoWeb: infrastructure for confluence tools (2018)
  3. Felgenhauer, Bertram; Thiemann, René: Reachability, confluence, and termination analysis with state-compatible automata (2017)
  4. Iborra, José; Nishida, Naoki; Vidal, Germán; Yamada, Akihisa: Relative termination via dependency pairs (2017)
  5. Lucas, Salvador; Meseguer, José: Dependency pairs for proving termination properties of conditional term rewriting systems (2017)
  6. Moser, Georg: KBOs, ordinals, subrecursive hierarchies and all that (2017)
  7. Sabel, David; Zantema, Hans: Termination of cycle rewriting by transformation and matrix interpretation (2017)
  8. Sternagel, Christian; Sternagel, Thomas: Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems (2017)
  9. Ábrahám, Erika; Kremer, Gereon: Satisfiability checking: theory and applications (2016)
  10. Aoto, Takahito; Kikuchi, Kentaro: Nominal confluence tool (2016)
  11. Avanzini, Martin; Moser, Georg: A combination framework for complexity (2016)
  12. Yamada, Akihisa; Sternagel, Christian; Thiemann, René; Kusakari, Keiichirou: AC dependency pairs revisited (2016)
  13. Gutiérrez, Raúl; Lucas, Salvador: Function calls at frozen positions in termination of context-sensitive rewriting (2015)
  14. Iborra, José; Nishida, Naoki; Vidal, Germán; Yamada, Akihisa: Reducing relative termination to dependency pair problems (2015)
  15. Zankl, Harald; Winkler, Sarah; Middeldorp, Aart: Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations (2015)
  16. Kordy, Barbara; Mauw, Sjouke; Radomirović, Saša; Schweitzer, Patrick: Attack-defense trees (2014)
  17. Neurauter, Friedrich; Middeldorp, Aart: Polynomial interpretations over the natural, rational and real numbers revisited (2014)
  18. Zankl, Harald; Korp, Martin: Modular complexity analysis for term rewriting (2014)
  19. Aoto, Takahito: Disproving confluence of term rewriting systems by interpretation and ordering (2013)
  20. Bofill, Miquel; Borralleras, Cristina; Rodríguez-Carbonell, Enric; Rubio, Albert: The recursive path and polynomial ordering for first-order and higher-order terms (2013)

1 2 3 4 5 next