Tyrolean

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

Showing results 1 to 20 of 69.
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. Sternagel, Christian; Sternagel, Thomas: Certifying confluence of quasi-decreasing strongly deterministic conditional term rewrite systems (2017)
  7. Aoto, Takahito; Kikuchi, Kentaro: Nominal confluence tool (2016)
  8. Avanzini, Martin; Moser, Georg: A combination framework for complexity (2016)
  9. Gutiérrez, Raúl; Lucas, Salvador: Function calls at frozen positions in termination of context-sensitive rewriting (2015)
  10. Iborra, José; Nishida, Naoki; Vidal, Germán; Yamada, Akihisa: Reducing relative termination to dependency pair problems (2015)
  11. Zankl, Harald; Winkler, Sarah; Middeldorp, Aart: Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations (2015)
  12. Kordy, Barbara; Mauw, Sjouke; Radomirović, Saša; Schweitzer, Patrick: Attack-defense trees (2014)
  13. Neurauter, Friedrich; Middeldorp, Aart: Polynomial interpretations over the natural, rational and real numbers revisited (2014)
  14. Zankl, Harald; Korp, Martin: Modular complexity analysis for term rewriting (2014)
  15. Aoto, Takahito: Disproving confluence of term rewriting systems by interpretation and ordering (2013)
  16. Bofill, Miquel; Borralleras, Cristina; Rodríguez-Carbonell, Enric; Rubio, Albert: The recursive path and polynomial ordering for first-order and higher-order terms (2013)
  17. Hirokawa, Nao; Middeldorp, Aart; Zankl, Harald: Uncurrying for termination and complexity (2013)
  18. Winkler, Sarah; Sato, Haruhiko; Middeldorp, Aart; Kurihara, Masahito: Multi-completion with termination tools (2013)
  19. Bouhoula, Adel; Jacquemard, Florent: Sufficient completeness verification for conditional and constrained TRS (2012)
  20. Codish, Michael; Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René: SAT solving for termination proofs with recursive path orders and dependency pairs (2012)

1 2 3 4 next