TPA: Termination Proved Automatically. TPA is a tool for proving termination of term rewrite systems (TRSs) in a fully automated fashion. The distinctive feature of TPA is the support for relative termination and the use of the technique of semantic labelling with natural numbers. Thanks to the latter, TPA is capable of delivering automated termination proofs for some difficult TRSs for which all other tools fail.
Keywords for this software
References in zbMATH (referenced in 12 articles , 1 standard article )
Showing results 1 to 12 of 12.
- Iborra, José; Nishida, Naoki; Vidal, Germán; Yamada, Akihisa: Relative termination via dependency pairs (2017)
- Iborra, José; Nishida, Naoki; Vidal, Germán; Yamada, Akihisa: Reducing relative termination to dependency pair problems (2015)
- Sternagel, Christian; Thiemann, René: Modular and certified semantic labeling and unlabeling (2011)
- Nishida, Naoki; Vidal, Germán: Termination of narrowing via termination of rewriting (2010)
- Durán, Francisco; Lucas, Salvador; Meseguer, José: Methods for proving termination of rewriting-based programming languages by transformation (2009)
- Koprowski, Adam; Waldmann, Johannes: Max/Plus tree automata for termination of term rewriting (2009)
- Zankl, Harald; Sternagel, Christian; Middeldorp, Aart: Transforming SAT into termination of rewriting (2009)
- Koprowski, Adam; Zantema, Hans: Certification of proving termination of term rewriting by matrix interpretations (2008)
- Lucas, Salvador; Meseguer, José: Termination of just/fair computations in term rewriting (2008)
- Hirokawa, Nao; Middeldorp, Aart: Tyrolean termination tool: techniques and features (2007)
- Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan: Mechanizing and improving dependency pairs (2006)
- Koprowski, Adam: TPA: termination proved automatically (2006)