Matrix interpretations for proving termination of term rewriting
From MaRDI portal
Recommendations
- Matrix Interpretations for Proving Termination of Term Rewriting
- Improved matrix interpretation
- Revisiting matrix interpretations for proving termination of term rewriting
- Termination of String Rewriting with Matrix Interpretations
- From Matrix Interpretations over the Rationals to Matrix Interpretations over the Naturals
Cites work
- scientific article; zbMATH DE number 3729436 (Why is no real title available?)
- Automating the dependency pair method
- Logic for Programming, Artificial Intelligence, and Reasoning
- Matrix Interpretations for Proving Termination of Term Rewriting
- Processes, terms and cycles: steps on the road to infinity. Essays dedicated to Jan Willem Klop on the occasion of his 60th birthday
- Rewriting Techniques and Applications
- Term Rewriting and Applications
- Termination of String Rewriting with Matrix Interpretations
- Termination of \(\{aa\rightarrow bc,bb\rightarrow ac,cc\rightarrow ab\}\)
- Termination of term rewriting using dependency pairs
- Termination of term rewriting: Interpretation and type elimination
- Theory and Applications of Satisfiability Testing
- Uncurrying for Termination
Cited in
(61)- Using linear constraints for logic program termination analysis
- AC completion with termination tools
- Certification of Proving Termination of Term Rewriting by Matrix Interpretations
- Context-sensitive dependency pairs
- KBO orientability
- Automatic generation of logical models with AGES
- Encoding dependency pair techniques and control strategies for maximal completion
- Joint spectral radius theory for automated complexity analysis of rewrite systems
- Term orderings for non-reachability of (conditional) rewriting
- Proving termination of graph transformation systems using weighted type graphs over semirings
- Improved matrix interpretation
- Lazy productivity via termination
- Decreasing diagrams and relative termination
- Proving termination by dependency pairs and inductive theorem proving
- Increasing interpretations
- Local Termination
- Checking termination of bottom-up evaluation of logic programs with function symbols
- Size-based termination of higher-order rewriting
- A dependency pair framework for innermost complexity analysis of term rewrite systems
- Decreasing diagrams and relative termination
- Matrix Interpretations for Proving Termination of Term Rewriting
- Normalization of Infinite Terms
- Derivational complexity and context-sensitive Rewriting
- Increasing Interpretations
- Logic programming with function symbols: checking termination of bottom-up evaluation through program adornments
- An automated approach to the Collatz conjecture
- On the domain and dimension hierarchy of matrix interpretations
- Arctic Termination ...Below Zero
- Maximal Termination
- An automated approach to the Collatz conjecture
- Reducing relative termination to dependency pair problems
- Dependency Pairs and Polynomial Path Orders
- Revisiting matrix interpretations for proving termination of term rewriting
- Transforming SAT into termination of rewriting
- System description: E.T. 0.1
- The Derivational Complexity Induced by the Dependency Pair Method
- On probabilistic term rewriting
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Termination of narrowing via termination of rewriting
- A new order-theoretic characterisation of the polytime computable functions
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Analyzing innermost runtime complexity of term rewriting by dependency pairs
- Relative termination via dependency pairs
- Automatic proofs of termination with elementary interpretations
- Uncurrying for termination and complexity
- Harnessing first order termination provers using higher order dependency pairs
- Automatic Termination
- The 2D dependency pair framework for conditional rewrite systems. II: Advanced processors and implementation techniques
- Tuple interpretations for termination of term rewriting
- Termination of cycle rewriting by transformation and matrix interpretation
- Automatic synthesis of logical models for order-sorted first-order theories
- mu-term: Verify Termination Properties Automatically (System Description)
- Beyond polynomials and Peano arithmetic -- automation of elementary and ordinal interpretations
- Applications and extensions of context-sensitive rewriting
- Termination of String Rewriting with Matrix Interpretations
- From Jinja bytecode to term rewriting: a complexity reflecting transformation
- Termination of Isabelle functions via termination of rewriting
- Termination by Quasi-periodic Interpretations
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
- Multi-dimensional interpretations for termination of term rewriting
- A Perron-Frobenius theorem for deciding matrix growth
This page was built for publication: Matrix interpretations for proving termination of term rewriting
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q928655)
