Tuple interpretations for termination of term rewriting
From MaRDI portal
Publication:2102931
DOI10.1007/s10817-022-09640-4OpenAlexW4287577798MaRDI QIDQ2102931
Publication date: 12 December 2022
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-022-09640-4
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Mechanizing and improving dependency pairs
- Matrix interpretations for proving termination of term rewriting
- Termination of term rewriting: Interpretation and type elimination
- Automatic synthesis of logical models for order-sorted first-order theories
- Termination of term rewriting using dependency pairs
- Multi-dimensional interpretations for termination of term rewriting
- Analyzing program termination and complexity automatically with \textsf{AProVE}
- Dynamic Dependency Pairs for Algebraic Functional Systems
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
- Satisfiability Modulo Theories
- Certification of Termination Proofs Using CeTA
- Improved Matrix Interpretation
- Maximal Termination
- Termination of String Rewriting with Matrix Interpretations
- Term Rewriting and All That
- mu-term: Verify Termination Properties Automatically (System Description)
- Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
- Nagoya Termination Tool
- A SAT-Based Approach to Size Change Termination with Global Ranking Functions
- Artificial Intelligence and Symbolic Computation
- Logic for Programming, Artificial Intelligence, and Reasoning
- Rewriting Techniques and Applications
- The termination hierarchy for term rewriting
- Tuple Interpretations for Higher-Order Complexity.
This page was built for publication: Tuple interpretations for termination of term rewriting
