Certification of Proving Termination of Term Rewriting by Matrix Interpretations

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

Hans Zantema, Adam Koprowski

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

68Q42: Grammars and rewriting systems

Related Items

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

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