Sciweavers

87
Voted
CORR
2006
Springer
95views Education» more  CORR 2006»
14 years 8 months ago
SAT Solving for Argument Filterings
Abstract. This paper introduces a propositional encoding for lexicographic path orders in connection with dependency pairs. This facilitates the application of SAT solvers for term...
Michael Codish, Peter Schneider-Kamp, Vitaly Lagoo...
83
Voted
RTA
2004
Springer
15 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...
129
Voted
LPAR
2004
Springer
15 years 2 months ago
The Dependency Pair Framework: Combining Techniques for Automated Termination Proofs
The dependency pair approach is one of the most powerful techniques for automated termination proofs of term rewrite systems. Up to now, it was regarded as one of several possible ...
Jürgen Giesl, René Thiemann, Peter Sch...
LOPSTR
2009
Springer
15 years 3 months ago
Goal-Directed and Relative Dependency Pairs for Proving the Termination of Narrowing
In this work, we first consider a goal-oriented extension of the dependency pair framework for proving termination w.r.t. a given set of initial terms. Then, we introduce a new re...
José Iborra, Naoki Nishida, Germán V...