重写对策在基于HOL的形式化证明中的应用

摘要：

讨论了重写对策在基于高阶逻辑定理证明系统HOL的形式化证明过程中的应用.通过REWRITE_ TAC对策、ASM_ REWRITE_ TAC对策和RW_ TAC对策,详细分析了重写对策的功能、应用方法、应用环境、应用中可能出现的问题以及解决办法,给出了DB.match搜索和DB.find搜索等重写对策的定理参数的选择方法,并进行了分析与比较.进一步说明了重写对策在基于HOL系统的形式化证明中的重要性,以期对HOL系统用户提供一些帮助与启发,促进HOL系统的进一步发展与完善,使形式化方法能够解决更多的实际问题.

关键词：定理证明方法、高阶逻辑定理证明系统、形式化证明、目标制导法、重写对策

所属期刊栏目：34

分类号：TP301.2(计算技术、计算机技术)

资助基金：国际科技合作与交流基金项目2011DFG13000

在线出版日期：2013-11-18（万方平台首次上网日期，不代表论文的发表时间）

页数：共5页

页码：3664-3668