• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>LIPIcs : Leibniz International Proceedings in Informatics >Certified Rule Labeling
【24h】

Certified Rule Labeling

机译：认证规则标签

获取原文
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The rule labeling heuristic aims to establish confluence of (left-)linear term rewrite systems via decreasing diagrams. We present a formalization of a confluence criterion based on the interplay of relative termination and the rule labeling in the theorem prover Isabelle. Moreover, we report on the integration of this result into the certifier CeTA, facilitating the checking of confluence certificates based on decreasing diagrams for the first time. The power of the method is illustrated by an experimental evaluation on a (standard) collection of confluence problems.
机译：规则标记试探法旨在通过减少图表来建立（左）线性术语重写系统的融合。我们基于定理证明者Isabelle中相对终止和规则标记之间的相互作用，提出合流标准的形式化。此外，我们报告了将该结果集成到认证机构CeTA中的情况，从而首次帮助基于减少图表的融合证书检查。通过对汇合问题的（标准）集合进行实验评估，说明了该方法的强大功能。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号