Certification of Proving Termination of Term Rewriting by Matrix Interpretations

DOI10.1007/978-3-540-77566-9_28MaRDI QIDQ5448658zbMATH OpenOpenAlexFDO

Authors Adam Koprowski, Hans Zantema

Publication date 7 March 2008

Published in SOFSEM 2008: Theory and Practice of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-77566-9_28

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• Matrix Interpretations for Proving Termination of Term Rewriting
• Matrix interpretations for proving termination of term rewriting
• Revisiting matrix interpretations for proving termination of term rewriting
• Improved matrix interpretation
• Max/Plus tree automata for termination of term rewriting

Cites work

• Certification of Automated Termination Proofs
• Certification of Proving Termination of Term Rewriting by Matrix Interpretations
• Certified Size-Change Termination
• Interacting with Modal Logics in the Coq Proof Assistant
• Logic for Programming, Artificial Intelligence, and Reasoning
• Matrix Interpretations for Proving Termination of Term Rewriting
• Termination of term rewriting using dependency pairs
• TPA: Termination Proved Automatically
• Tyrolean termination tool: techniques and features

Cited in

(10)

• Certifying term rewriting proofs in ELAN
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
• Arctic Termination ...Below Zero
• Certification of Automated Termination Proofs
• Matrix Interpretations for Proving Termination of Term Rewriting
• Automatic Termination
• Local Termination
• Automated certified proofs with CiME3
• Certification of Proving Termination of Term Rewriting by Matrix Interpretations
• Coq formalization of the higher-order recursive path ordering

Describes a project that uses

Uses Software

• Coq
• CoLoR
• TPDB
• Tyrolean
• CiME
• TPA

This page was built for publication: Certification of Proving Termination of Term Rewriting by Matrix Interpretations

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5448658)