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

• 作者: 段振华 马倩
• 来源期刊: 西安电子科技大学学报（自然科学版）
• 学科: 工学
• 关键词: 时序逻辑 公理系统 定理证明 验证
• 年，卷（期）: 2016,（1）
• 页码范围: 75-81
• 页数: 7页
• 分类号: TP301
• 字数: 5925字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-2400.2016.01.014

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	段振华	西安电子科技大学计算理论与技术研究所	47	363	10.0	16.0
2	马倩	西安电子科技大学计算理论与技术研究所	2	5	1.0	2.0