Uncurrying for termination and complexity

DOI10.1007/S10817-012-9248-3zbMath1286.68262OpenAlexW1983193642MaRDI QIDQ352959

Aart Middeldorp, Nao Hirokawa, Harald Zankl

Publication date: 5 July 2013

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

Full work available at URL: https://doi.org/10.1007/s10817-012-9248-3

zbMATH Keywords

terminationterm rewritinguncurrying

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items (4)

A combination framework for complexity ⋮ Uncurrying for termination and complexity ⋮ Unnamed Item ⋮ A Lambda-Free Higher-Order Recursive Path Order

Uses Software

• Tyrolean

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Uncurrying for termination and complexity
• Modular properties of conditional term rewriting systems
• Tyrolean termination tool: techniques and features
• Mechanizing and improving dependency pairs
• Matrix interpretations for proving termination of term rewriting
• Normalization results for typeable rewrite systems
• Some characteristics of strong innermost normalization
• Comparing curried and uncurried rewriting
• Termination of term rewriting using dependency pairs
• Enhancing dependency pair method using strong computability in simply-typed term rewriting
• Automating the dependency pair method
• Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems
• Satisfiability of Non-linear (Ir)rational Arithmetic
• Complexity Analysis of Term Rewriting Based on Matrix and Context Dependent Interpretations
• Generalized and Formalized Uncurrying
• HORPO with Computability Closure: A Reconstruction
• Automated Complexity Analysis Based on the Dependency Pair Method
• Polymorphic higher-order recursive path orderings
• Signature Extensions Preserve Termination
• Term Rewriting and All That
• Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting
• Higher Order Dependency Pairs for Algebraic Functional Systems
• POLYNOMIALLY BOUNDED MATRIX INTERPRETATIONS
• Modular Complexity Analysis via Relative Complexity
• Random Descent
• Frontiers of Combining Systems
• Uncurrying for Termination
• Term Rewriting and Applications
• Logic for Programming, Artificial Intelligence, and Reasoning
• Rewriting Techniques and Applications
• The Derivational Complexity Induced by the Dependency Pair Method

This page was built for publication: Uncurrying for termination and complexity