Automated Complexity Analysis Based on the Dependency Pair Method

DOI10.1007/978-3-540-71070-7_32zbMath1165.68390arXiv1102.3129OpenAlexW1913470731MaRDI QIDQ3541717

Georg Moser, Nao Hirokawa

Publication date: 27 November 2008

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1102.3129

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (26)

A combination framework for complexity ⋮ Unnamed Item ⋮ ATLAS: automated amortised complexity analysis of self-adjusting data structures ⋮ On sharing, memoization, and polynomial time ⋮ From Jinja bytecode to term rewriting: a complexity reflecting transformation ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Uncurrying for termination and complexity ⋮ Lower bounds for runtime complexity of term rewriting ⋮ Reversible computation in term rewriting ⋮ Analyzing Innermost Runtime Complexity Through Tuple Interpretations ⋮ Analysing parallel complexity of term rewriting ⋮ Proving Quadratic Derivational Complexities Using Context Dependent Interpretations ⋮ A Perron-Frobenius theorem for deciding matrix growth ⋮ Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems ⋮ A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems ⋮ Constant runtime complexity of term rewriting is semi-decidable ⋮ Applications and extensions of context-sensitive rewriting ⋮ Dependency Pairs and Polynomial Path Orders ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates ⋮ The Derivational Complexity Induced by the Dependency Pair Method ⋮ Derivational complexity and context-sensitive Rewriting ⋮ Characterizing Compatible View Updates in Syntactic Bidirectionalization ⋮ A new order-theoretic characterisation of the polytime computable functions ⋮ Real or natural number interpretation and their effect on complexity ⋮ Analyzing innermost runtime complexity of term rewriting by dependency pairs ⋮ Runtime complexity analysis of logically constrained rewriting

Uses Software

• Tyrolean

Cites Work

• Unnamed Item
• Unnamed Item
• Termination proofs for term rewriting systems by lexicographic path orderings imply multiply recursive derivation lengths
• Mechanically proving termination using polynomial interpretations
• Tyrolean termination tool: techniques and features
• On tree automata that certify termination of left-linear term rewriting systems
• Mechanizing and improving dependency pairs
• Termination proofs by multiset path orderings imply primitive recursive derivation lengths
• Modular termination proofs for rewriting using dependency pairs
• Termination of term rewriting using dependency pairs
• Algorithms with polynomial interpretation termination proof
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Termination proofs and the length of derivations
• Derivational Complexity of Knuth-Bendix Orders Revisited
• Complexity Analysis by Rewriting

This page was built for publication: Automated Complexity Analysis Based on the Dependency Pair Method