程序验证中归纳性质定理的自动证明

• 作者: 郝爔
• 来源期刊: 电子技术
• 关键词: 程序验证 归纳定理 自动定理证明 结构归纳
• 年，卷（期）: 2015,（8）
• 所属期刊栏目: 电子技术研发
• 页码范围: 1-6
• 页数: 6页
• 字数: 7282字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-0755.2015.08.001

摘要

基于演绎推理的程序验证系统原型的功能往往受限于断言语言的表达能力、循环不变式的自动推断能力和自动定理证明器的证明能力。文章为了增强程序断言语言对程序性质的表达能力，为系统原型引入了自定义归纳谓词。此外，为了减轻自动定理证明器的压力，文章提出由程序员提供自定义谓词之间的归纳性质定理来帮助自动定理证明器的方式。由于性质定理是程序员提供的，无法保证其正确性，文章采取了一种对性质定理先分析后结构归纳的方法，实现了性质定理的自动证明。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郝爔	中国科学技术大学计算机科学与技术学院	1	0	0.0	0.0