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

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