AProVE 1.2: Automatic Termination Proofs in the Dependency Pair Framework. AProVE 1.2 is one of the most powerful systems for automated termination proofs of term rewrite systems (TRSs). It is the first tool which automates the new dependency pair framework  and therefore permits a completely flexible combination of different termination proof techniques. Due to this framework, AProVE 1.2 is also the first termination prover which can be fully configured by the user.
Keywords for this software
References in zbMATH (referenced in 148 articles , 1 standard article )
Showing results 141 to 148 of 148.
- Lucas, Salvador: Polynomials over the reals in proofs of termination: from theory to practice (2005)
- Nishida, Naoki; Sakai, Masahiko; Sakabe, Toshiki: Partial inversion of constructor term rewriting systems (2005)
- Thiemann, René; Giesl, Jürgen: The size-change principle and dependency pairs for termination of term rewriting (2005)
- Zantema, H.: Termination of string rewriting proved automatically (2005)
- Giesl, Jürgen; Thiemann, René; Schneider-Kamp, Peter; Falke, Stephan: Automated termination proofs with AProVE (2004) ioport
- 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)
- Lee, Chin Soon: Program termination analysis in polynomial time (2002)
Further publications can be found at: http://aprove.informatik.rwth-aachen.de/index.asp?subform=references.html