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