Multi-dimensional interpretations for termination of term rewriting

DOI10.1007/978-3-030-79876-5_16OpenAlexW3177571835MaRDI QIDQ2055861

Akihisa Yamada

Publication date: 1 December 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-79876-5_16

Mathematics Subject Classification ID

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

• z3
• CeTA
• Tyrolean
• StarExec
• CoLoR
• MU-TERM
• NaTT

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