Certification of Proving Termination of Term Rewriting by Matrix Interpretations

DOI10.1007/978-3-540-77566-9_28zbMath1132.68431OpenAlexW2067772798MaRDI QIDQ5448658

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

Related Items (6)

Coq formalization of the higher-order recursive path ordering ⋮ Arctic Termination ...Below Zero ⋮ Certification of Proving Termination of Term Rewriting by Matrix Interpretations ⋮ Automatic Termination ⋮ Local Termination ⋮ CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates

Uses Software

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

Cites Work

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

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