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

文章基本信息

  • 标题:Certified Subterm Criterion and Certified Usable Rules
  • 本地全文:下载
  • 作者:Christian Sternagel ; Ren{\'e} Thiemann
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2010
  • 卷号:6
  • 页码:325-340
  • DOI:10.4230/LIPIcs.RTA.2010.325
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:In this paper we present our formalization of two important termination techniques for term rewrite systems: the subterm criterion and the reduction pair processor in combination with usable rules. For both techniques we developed executable check functions in the theorem prover Isabelle/HOL which can certify the correct application of these techniques in some given termination proof. As there are several variants of usable rules we designed our check function in such a way that it accepts all known variants, even those which are not explicitly spelled out in previous papers. We integrated our formalization in the publicly available IsaFoR-library. This led to a significant increase in the power of CeTA, the corresponding certified termination proof checker that is extracted from IsaFoR.
  • 关键词:Term Rewriting; Certification; Termination; Theorem Proving
国家哲学社会科学文献中心版权所有