Tsukuba

Tsukuba Termination Tool. We present a tool for automatically proving termination of first-order rewrite systems. The tool is based on the dependency pair method of Arts and Giesl. It incorporates several new ideas that make the method more efficient. The tool produces high-quality output and has a convenient web interface.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 10 articles )

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

  1. Durán, Francisco; Lucas, Salvador; Marché, Claude; Meseguer, José; Urbain, Xavier: Proving operational termination of membership equational programs (2008)
  2. Hirokawa, Nao; Middeldorp, Aart: Tyrolean termination tool: techniques and features (2007)
  3. Chiba, Yuki; Aoto, Takahito: RAPT: A program transformation system based on term rewriting (2006)
  4. Contejean, Evelyne; Marché, Claude; Tomás, Ana Paula; Urbain, Xavier: Mechanically proving termination using polynomial interpretations (2005)
  5. Hirokawa, Nao; Middeldorp, Aart: Automating the dependency pair method (2005)
  6. Nishida, Naoki; Sakai, Masahiko; Sakabe, Toshiki: Partial inversion of constructor term rewriting systems (2005)
  7. Zantema, H.: Termination of string rewriting proved automatically (2005)
  8. Thiemann, René; Giesl, Jürgen; Schneider-Kamp, Peter: Improved modular termination proofs using dependency pairs (2004)
  9. Urbain, Xavier: Modular and incremental automated termination proofs (2004)
  10. Hirokawa, Nao; Middeldorp, Aart: Tsukuba termination tool (2003)