IANDC
2007
14 years 11 days ago
2007
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...
CORR
2006
Springer
14 years 14 days ago
2006
Springer
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...
CADE
2001
Springer
14 years 5 months ago
2001
Springer
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...
RTA
2004
Springer
14 years 5 months ago
2004
Springer
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...
RTA
2004
Springer
14 years 5 months ago
2004
Springer
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...
SOFSEM
2007
Springer
14 years 6 months ago
2007
Springer
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...
RTA
2009
Springer
14 years 7 months ago
2009
Springer
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...
CADE
2003
Springer
15 years 22 days ago
2003
Springer
Developing automatable methods for proving termination of term rewrite systems that resist traditional techniques based on simplification orders has become an active research area ...
CADE
2007
Springer
15 years 22 days ago
2007
Springer
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...