Sciweavers

Share
RTA
2010
Springer
8 years 7 months ago
Modular Complexity Analysis via Relative Complexity
Abstract. In this paper we introduce a modular framework which allows to infer (feasible) upper bounds on the (derivational) complexity of term rewrite systems by combining differ...
Harald Zankl, Martin Korp
LICS
1994
IEEE
8 years 7 months ago
Higher-Order Narrowing
Higher-order narrowing is a general method for higher-order equational reasoning and serves for instance as the foundation for the integration of functional and logic programming. ...
Christian Prehofer
CADE
2001
Springer
8 years 8 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
8 years 8 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
FROCOS
2005
Springer
8 years 9 months ago
Proving Liveness with Fairness Using Rewriting
Abstract. In this paper we combine rewriting techniques with verification issues. More precisely, we show how techniques for proving relative termination of term rewrite systems (...
Adam Koprowski, Hans Zantema
BIRTHDAY
2005
Springer
8 years 9 months ago
Reducing Right-Hand Sides for Termination
We propose two transformations on term rewrite systems (TRSs) based on reducing right hand sides: one related to the transformation order and a variant of dummy elimination. Under ...
Hans Zantema
CADE
2007
Springer
8 years 9 months ago
Proving Termination by Bounded Increase
Abstract. Most methods for termination analysis of term rewrite systems (TRSs) essentially try to find arguments of functions that decrease in recursive calls. However, they fail ...
Jürgen Giesl, René Thiemann, Stephan S...
RTA
2009
Springer
8 years 10 months ago
Loops under Strategies
Most techniques to automatically disprove termination of term rewrite systems search for a loop. Whereas a loop implies nontermination for full rewriting, this is not necessarily t...
René Thiemann, Christian Sternagel
CADE
2003
Springer
9 years 3 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
2008
Springer
9 years 3 months ago
Modularity of Confluence
We present a novel proof of Toyama's famous modularity of confluence result for term rewriting systems. Apart from being short and intuitive, the proof is modular itself in th...
Vincent van Oostrom
books