Sciweavers

Share
IANDC
2007
106views more  IANDC 2007»
9 years 9 months ago
Tyrolean termination tool: Techniques and features
The Tyrolean Termination Tool (TTT for short) is a powerful tool for automatically proving termination of rewrite systems. It incorporates several new refinements of the dependen...
Nao Hirokawa, Aart Middeldorp
CORR
2006
Springer
95views Education» more  CORR 2006»
9 years 9 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...
CADE
2001
Springer
10 years 2 months ago
Approximating Dependency Graphs Using Tree Automata Techniques
The dependency pair method of Arts and Giesl is the most powerful technique for proving termination of term rewrite systems automatically. We show that the method can be improved b...
Aart Middeldorp
RTA
2004
Springer
10 years 3 months ago
TORPA: Termination of Rewriting Proved Automatically
Abstract. In this paper it is described how a combination of polynomial interpretations, recursive path order, RFC match-bounds, the dependency pair method and semantic labelling c...
Hans Zantema
RTA
2004
Springer
10 years 3 months ago
Dependency Pairs Revisited
Abstract. In this paper we present some new refinements of the dependency pair method for automatically proving the termination of term rewrite systems. These refinements are ver...
Nao Hirokawa, Aart Middeldorp
SOFSEM
2007
Springer
10 years 3 months ago
Constraints for Argument Filterings
Abstract. The dependency pair method is a powerful method for automatically proving termination of rewrite systems. When used with traditional simplification orders like LPO and K...
Harald Zankl, Nao Hirokawa, Aart Middeldorp
RTA
2009
Springer
10 years 4 months ago
The Derivational Complexity Induced by the Dependency Pair Method
We study the derivational complexity induced by the (basic) dependency pair method. Suppose the derivational complexity induced by a termination method is closed under elementary f...
Georg Moser, Andreas Schnabl
CADE
2003
Springer
10 years 10 months ago
Automating the Dependency Pair Method
Developing automatable methods for proving termination of term rewrite systems that resist traditional techniques based on simplification orders has become an active research area ...
Nao Hirokawa, Aart Middeldorp
CADE
2007
Springer
10 years 10 months ago
Dependency Pairs for Rewriting with Non-free Constructors
Abstract. A method based on dependency pairs for showing termination of functional programs on data structures generated by constructors with relations is proposed. A functional pr...
Stephan Falke, Deepak Kapur
books