MSVL程序的自动定理证明方法

作     者：马倩 段振华 MA Qian;DUAN Zhenhua

作者机构：西安电子科技大学计算理论与技术研究所陕西西安710071 

基　　金：国家自然科学基金资助项目(61133001 61272117 61202038) 

出 版 物：《西安电子科技大学学报》 (Journal of Xidian University)

年 卷 期：2016年第43卷第1期

页      码：75-81页

摘      要：时序逻辑程序设计语言能被用于验证C、Verilog/VHDL程序的正确性.但目前时序逻辑程序设计语言程序只能纯手工进行定理证明.针对该问题提出了一种基于定理证明器原型验证系统的时序逻辑程序设计语言程序的自动定理证明方法.该方法首先使用原型验证系统规范语言描述时序逻辑程序设计语言的语法和语义,使得原型验证系统能够正确识别时序逻辑程序设计语言程序;然后使用原型验证系统规范语言描述时序逻辑程序设计语言的公理系统和待证定理;最后输入原型验证系统命令调用原型验证系统证明器来进行时序逻辑程序设计语言程序的推演证明.在证明过程中,细节被原型验证系统自动地证明,使得人工仅在复杂的步骤上指导控制,从而实现半自动地验证时序逻辑程序设计语言程序,简化了该定理的证明过程.

主 题 词：时序逻辑 公理系统 定理证明 验证 

学科分类：0808[工学-自动化类] 0809[工学-计算机类] 08[工学] 0812[工学-测绘类] 081202[081202] 

核心收录：

D　O　I：10.3969/j.issn.1001-2400.2016.01.014

馆 藏 号：203920893...