Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL
复制标题
在 Isabelle/HOL 中查找终止证明的词典顺序
DOI：
--
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
T. Nipkow
中科院分区：
文献类型：
--
作者：
Lukas Bulwahn;Alexander Krauss;T. Nipkow
我们提出了一个简单的方法来正式证明递归函数的终止搜索字典组合的大小措施。尽管它的简单，该方法被证明是强大的，足以解决日常定理证明实践中遇到的绝大多数终止问题。
We present a simple method to formally prove termination of recursive functions by searching for lexicographic combinations of size measures. Despite its simplicity, the method turns out to be powerful enough to solve a large majority of termination problems encountered in daily theorem proving practice.