10.3969/j.issn.1000-7024.2013.10.058
重写对策在基于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