Multi-dimensional interpretations for termination of term rewriting
From MaRDI portal
Publication:2055861
DOI10.1007/978-3-030-79876-5_16OpenAlexW3177571835MaRDI QIDQ2055861
Publication date: 1 December 2021
Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_16
Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (2)
Tuple interpretations for termination of term rewriting ⋮ Term orderings for non-reachability of (conditional) rewriting
Uses Software
Cites Work
- 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
- 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
- Proving Termination of Programs Automatically with AProVE
- Improved Matrix Interpretation
- Maximal Termination
- Termination of String Rewriting with Matrix Interpretations
- Term Rewriting and All That
- Formalizing Monotone Algebras for Certification of Termination and Complexity Proofs
- Nagoya Termination Tool
- Artificial Intelligence and Symbolic Computation
- Logic for Programming, Artificial Intelligence, and Reasoning
- Rewriting Techniques and Applications
- The termination hierarchy for term rewriting
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Multi-dimensional interpretations for termination of term rewriting
