Tuple interpretations for termination of term rewriting
From MaRDI portal
Publication:2102931
Recommendations
Cites work
- A SAT-Based Approach to Size Change Termination with Global Ranking Functions
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Artificial Intelligence and Symbolic Computation
- Automated certified proofs with CiME3
- Automatic synthesis of logical models for order-sorted first-order theories
- Certification of Termination Proofs Using CeTA
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
- Dynamic dependency pairs for algebraic functional systems
- Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
- scientific article; zbMATH DE number 1487842 (Why is no real title available?)
- Improved matrix interpretation
- Logic for Programming, Artificial Intelligence, and Reasoning
- Matrix interpretations for proving termination of term rewriting
- Max/Plus tree automata for termination of term rewriting
- Maximal Termination
- Mechanizing and improving dependency pairs
- mu-term: Verify Termination Properties Automatically (System Description)
- Multi-dimensional interpretations for termination of term rewriting
- Nagoya termination tool
- Rewriting Techniques and Applications
- Satisfiability modulo theories
- Term Rewriting and All That
- Termination of String Rewriting with Matrix Interpretations
- Termination of term rewriting using dependency pairs
- Termination of term rewriting: Interpretation and type elimination
- The termination hierarchy for term rewriting
- Tuple Interpretations for Higher-Order Complexity.
Cited in
(7)- Increasing interpretations
- Multi-dimensional interpretations for termination of term rewriting
- Increasing Interpretations
- Analyzing Innermost Runtime Complexity Through Tuple Interpretations
- A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems
- Termination of graph transformation systems using weighted subgraph counting
- Higher-order constrained dependency pairs for (universal) computability
Describes a project that uses
Uses Software
This page was built for publication: Tuple interpretations for termination of term rewriting
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2102931)
