Multi-dimensional interpretations for termination of term rewriting

DOI10.1007/978-3-030-79876-5_16MaRDI QIDQ2055861zbMATH OpenOpenAlexFDO

Authors Akihisa Yamada

Publication date 1 December 2021

Copyright license Creative Commons Attribution 4.0 International

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)

Recommendations

• Tuple interpretations for termination of term rewriting
• Termination of term rewriting by interpretation
• Matrix interpretations for proving termination of term rewriting
• Matrix Interpretations for Proving Termination of Term Rewriting
• Improved matrix interpretation

Cites work

• 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
• Nagoya termination tool
• Proving termination of programs automatically with AProVE
• 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

Cited in

(3)

• Tuple interpretations for termination of term rewriting
• Term orderings for non-reachability of (conditional) rewriting
• Multi-completion with termination tools

Describes a project that uses

Uses Software

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

This page was built for publication: Multi-dimensional 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 Q2055861)