JAR
2006
13 years 4 months ago
2006
The dependency pair technique [1, 11, 12] is a powerful method for automated termination and innermost termination proofs of term rewrite systems (TRSs). For any TRS, it generates ...
DAGSTUHL
2007
13 years 6 months ago
2007
Abstract. The dependency pair technique is a powerful modular method for automated termination proofs of term rewrite systems. We first show that dependency pairs are also suitabl...
PEPM
2010
ACM
13 years 6 months ago
2010
ACM
Software engineering, automated reasoning, rule-based programming or specifications often use rewriting systems for which termination, among other properties, may have to be ensur...
RTA
2004
Springer
13 years 10 months ago
2004
Springer
We describe the system AProVE, an automated prover to verify (innermost) termination of term rewrite systems (TRSs). For this system, we have developed and implemented efficient al...
CADE
2003
Springer
14 years 4 months ago
2003
Springer
Ordinals form the basis for termination proofs in ACL2. Currently, ACL2 uses a rather inefficient representation for the ordinals up to 0 and provides limited support for reasoning...
CADE
2006
Springer
14 years 4 months ago
2006
Springer
Abstract. Based on inductive definitions, we develop an automated tool for defining partial recursive functions in Higher-Order Logic and providing appropriate reasoning tools for ...
CADE
2007
Springer
14 years 4 months ago
2007
Springer
We develop a formalization of the Size-Change Principle in Isabelle/HOL and use it to construct formally certified termination proofs for recursive functions automatically.