Sciweavers

Share
JAR
2006
95views more  JAR 2006»
8 years 9 months ago
Mechanizing and Improving Dependency Pairs
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 ...
Jürgen Giesl, René Thiemann, Peter Sch...
DAGSTUHL
2007
8 years 10 months ago
Decision Procedures for Loop Detection
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...
René Thiemann, Jürgen Giesl, Peter Sch...
PEPM
2010
ACM
8 years 11 months ago
A3PAT, an approach for certified automated termination proofs
Software engineering, automated reasoning, rule-based programming or specifications often use rewriting systems for which termination, among other properties, may have to be ensur...
Evelyne Contejean, Andrey Paskevich, Xavier Urbain...
RTA
2004
Springer
9 years 2 months ago
Automated Termination Proofs with AProVE
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...
Jürgen Giesl, René Thiemann, Peter Sch...
CADE
2003
Springer
9 years 9 months ago
Algorithms for Ordinal Arithmetic
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...
Panagiotis Manolios, Daron Vroon
CADE
2006
Springer
9 years 9 months ago
Partial Recursive Functions in Higher-Order Logic
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 ...
Alexander Krauss
CADE
2007
Springer
9 years 9 months ago
Certified Size-Change Termination
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.
Alexander Krauss
books