Multi-completion with Termination Tools (System Description)

Multi-completion with Termination Tools (System Description)
复制标题

使用终止工具进行多重完成（系统描述）

DOI：
10.1007/978-3-540-71070-7_26
复制
发表时间：
2008
期刊：
--
影响因子：
--
通讯作者：
A. Middeldorp
A. Middeldorp
中科院分区：
--
文献类型：
--
作者：
Haruhiko Sato;S. Winkler;M. Kurihara;A. Middeldorp

文献摘要

被引文献

相似文献

在本文中，我们描述了一个新的工具，自动终止工具执行Knuth-Benidorm完成。它基于两个组成部分：（1）Kurihara和Kondo（1999）提出的多重约简序完备化推理系统;（2）Wehrman，Stump和Westbrook（2006）提出的外部终止证明器完备化推理系统，并在Slothrop系统中实现。我们的工具可以与满足某些最低要求的任何端接工具一起使用。初步的实验结果表明，我们的工具的潜力。
In this paper we describe a new tool for performing Knuth-Bendix completion with automatic termination tools. It is based on two ingredients: (1) the inference system for completion with multiple reduction orderings introduced by Kurihara and Kondo (1999) and (2) the inference system for completion with external termination provers proposed by Wehrman, Stump and Westbrook (2006) and implemented in theSlothropsystem. Our tool can be used with any termination tool that satisfies certain minimal requirements. Preliminary experimental results show the potential of our tool.