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

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

1 2 3 4 next

  1. Avanzini, Martin; Moser, Georg: A combination framework for complexity (2016)
  2. Iborra, José; Nishida, Naoki; Vidal, Germán; Yamada, Akihisa: Reducing relative termination to dependency pair problems (2015)
  3. Zankl, Harald; Winkler, Sarah; Middeldorp, Aart: Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations (2015)
  4. Kordy, Barbara; Mauw, Sjouke; Radomirović, Saša; Schweitzer, Patrick: Attack-defense trees (2014)
  5. Neurauter, Friedrich; Middeldorp, Aart: Polynomial interpretations over the natural, rational and real numbers revisited (2014)
  6. Zankl, Harald; Korp, Martin: Modular complexity analysis for term rewriting (2014)
  7. Aoto, Takahito: Disproving confluence of term rewriting systems by interpretation and ordering (2013)
  8. Bofill, Miquel; Borralleras, Cristina; Rodríguez-Carbonell, Enric; Rubio, Albert: The recursive path and polynomial ordering for first-order and higher-order terms (2013)
  9. Hirokawa, Nao; Middeldorp, Aart; Zankl, Harald: Uncurrying for termination and complexity (2013)
  10. Winkler, Sarah; Sato, Haruhiko; Middeldorp, Aart; Kurihara, Masahito: Multi-completion with termination tools (2013)
  11. Bouhoula, Adel; Jacquemard, Florent: Sufficient completeness verification for conditional and constrained TRS (2012)
  12. Codish, Michael; Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René: SAT solving for termination proofs with recursive path orders and dependency pairs (2012)
  13. Kop, Cynthia; van Raamsdonk, Femke: Dynamic dependency pairs for algebraic functional systems (2012)
  14. Fuhs, Carsten; Giesl, Jürgen; Parting, Michael; Schneider-Kamp, Peter; Swiderski, Stephan: Proving termination by dependency pairs and inductive theorem proving (2011)
  15. Fuhs, Carsten; Kop, Cynthia: Harnessing first order termination provers using higher order dependency pairs (2011)
  16. Hirokawa, Nao; Middeldorp, Aart: Decreasing diagrams and relative termination (2011)
  17. Moser, Georg; Schnabl, Andreas: The derivational complexity induced by the dependency pair method (2011)
  18. Moser, Georg; Schnabl, Andreas: Termination proofs in the dependency pair framework May induce multiple recursive derivational complexity (2011)
  19. Alarcón, Beatriz; Gutiérrez, Raúl; Lucas, Salvador: Context-sensitive dependency pairs (2010)
  20. Falke, Stephan; Kapur, Deepak: Termination of context-sensitive rewriting with built-in numbers and collection data structures (2010)

1 2 3 4 next