Termination Tools in Ordered Completion
Termination Tools in Ordered Completion
复制标题
有序完成中的终止工具
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
A. Middeldorp
中科院分区：
文献类型：
--
作者：
S. Winkler;A. Middeldorp
有序补全是方程定理证明中最常用的一种演算方法。有序完成运行的性能在很大程度上取决于作为输入提供的缩减顺序。本文描述了终止工具如何在有序完成过程中取代固定的减少订单，从而允许一种新的自动化程度。我们的方法可以与Kondo和Kurihara提出的多重完井方法相结合。本文给出了用有序补全工具omkbTT证明有序补全和方程定理的实验结果。
Ordered completion is one of the most frequently used calculi in equational theorem proving. The performance of an ordered completion run strongly depends on the reduction order supplied as input. This paper describes how termination tools can replace fixed reduction orders in ordered completion procedures, thus allowing for a novel degree of automation. Our method can be combined with the multi-completion approach proposed by Kondo and Kurihara. We present experimental results obtained with our ordered completion tool omkbTT for both ordered completion and equational theorem proving.