Matrix interpretations for proving termination of term rewriting
From MaRDI portal
Publication:928655
DOI10.1007/s10817-007-9087-9zbMath1139.68049OpenAlexW2136514805MaRDI QIDQ928655
Johannes Waldmann, Jörg Endrullis, Hans Zantema
Publication date: 11 June 2008
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://research.vu.nl/ws/files/2410076/219625.pdf
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Grammars and rewriting systems (68Q42)
Related Items (50)
Relative termination via dependency pairs ⋮ Analyzing program termination and complexity automatically with \textsf{AProVE} ⋮ mu-term: Verify Termination Properties Automatically (System Description) ⋮ Harnessing First Order Termination Provers Using Higher Order Dependency Pairs ⋮ Encoding Dependency Pair Techniques and Control Strategies for Maximal Completion ⋮ Reducing Relative Termination to Dependency Pair Problems ⋮ System Description: E.T. 0.1 ⋮ KBO orientability ⋮ From Jinja bytecode to term rewriting: a complexity reflecting transformation ⋮ SAT solving for termination proofs with recursive path orders and dependency pairs ⋮ Automatic synthesis of logical models for order-sorted first-order theories ⋮ Uncurrying for termination and complexity ⋮ Termination of Cycle Rewriting by Transformation and Matrix Interpretation ⋮ Size-based termination of higher-order rewriting ⋮ Proving Termination of Graph Transformation Systems Using Weighted Type Graphs over Semirings ⋮ Checking termination of bottom-up evaluation of logic programs with function symbols ⋮ Using linear constraints for logic program termination analysis ⋮ Proving termination by dependency pairs and inductive theorem proving ⋮ Decreasing diagrams and relative termination ⋮ Normalization of Infinite Terms ⋮ The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques ⋮ Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations ⋮ Logic programming with function symbols: Checking termination of bottom-up evaluation through program adornments ⋮ A Perron-Frobenius theorem for deciding matrix growth ⋮ Joint Spectral Radius Theory for Automated Complexity Analysis of Rewrite Systems ⋮ Termination of narrowing via termination of rewriting ⋮ Lazy productivity via termination ⋮ An automated approach to the Collatz conjecture ⋮ Decreasing Diagrams and Relative Termination ⋮ Context-sensitive dependency pairs ⋮ A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems ⋮ AC Completion with Termination Tools ⋮ Applications and extensions of context-sensitive rewriting ⋮ Termination of Isabelle Functions via Termination of Rewriting ⋮ Multi-dimensional interpretations for termination of term rewriting ⋮ An automated approach to the Collatz conjecture ⋮ Automatic generation of logical models with AGES ⋮ Automatic Termination ⋮ Dependency Pairs and Polynomial Path Orders ⋮ Local Termination ⋮ 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 ⋮ Transforming SAT into Termination of Rewriting ⋮ Derivational complexity and context-sensitive Rewriting ⋮ Increasing interpretations ⋮ Increasing Interpretations ⋮ Tuple interpretations for termination of term rewriting ⋮ Term orderings for non-reachability of (conditional) rewriting ⋮ A new order-theoretic characterisation of the polytime computable functions ⋮ Analyzing innermost runtime complexity of term rewriting by dependency pairs
Uses Software
Cites Work
- Unnamed Item
- Termination of \(\{aa\rightarrow bc,bb\rightarrow ac,cc\rightarrow ab\}\)
- Termination of term rewriting: Interpretation and type elimination
- Termination of term rewriting using dependency pairs
- Automating the dependency pair method
- Processes, terms and cycles: steps on the road to infinity. Essays dedicated to Jan Willem Klop on the occasion of his 60th birthday
- Termination of String Rewriting with Matrix Interpretations
- Matrix Interpretations for Proving Termination of Term Rewriting
- Uncurrying for Termination
- Term Rewriting and Applications
- Logic for Programming, Artificial Intelligence, and Reasoning
- Theory and Applications of Satisfiability Testing
- Rewriting Techniques and Applications
This page was built for publication: Matrix interpretations for proving termination of term rewriting
