首页    期刊浏览 2024年11月24日 星期日
登录注册

文章基本信息

  • 标题:Certifying the Weighted Path Order (Invited Talk)
  • 本地全文:下载
  • 作者:Ren Thiemann ; Jonas Sch{"o}pf ; Christian Sternagel
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2020
  • 卷号:167
  • 页码:4:1-4:20
  • DOI:10.4230/LIPIcs.FSCD.2020.4
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:The weighted path order (WPO) unifies and extends several termination proving techniques that are known in term rewriting. Consequently, the first tool implementing WPO could prove termination of rewrite systems for which all previous tools failed. However, we should not blindly trust such results, since there might be problems with the implementation or the paper proof of WPO. In this work, we increase the reliability of these automatically generated proofs. To this end, we first formally prove the properties of WPO in Isabelle/HOL, and then develop a verified algorithm to certify termination proofs that are generated by tools using WPO. We also include support for max-polynomial interpretations, an important ingredient in WPO. Here we establish a connection to an existing verified SMT solver. Moreover, we extend the termination tools NaTT and TTT2, so that they can now generate certifiable WPO proofs.
  • 关键词:certification; Isabelle/HOL; reduction order; termination analysis
国家哲学社会科学文献中心版权所有