程序正确性证明中逻辑公式的可满足性C

• 作者: 王彩芬
• 来源期刊: 西北师范大学学报(自然科学版)
• 学科: 工学
• 关键词: 程序正确性证明 Hoare公理系统 逻辑公式的可满足性
• 年，卷（期）: 2001,（3）
• 所属期刊栏目: 数学与计算机科学
• 页码范围: 27-32
• 页数: 6页
• 分类号: TP311
• 字数: 4737字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-988X.2001.03.006

摘要

采用Herbrand定理及归结原理证明在程序证明中遇到的逻辑公式是可满足的，并给出了相应的算法；同时讨论了已知循环程序中循环不变式的求解方法．

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王彩芬	西北师范大学数学与信息科学学院	183	820	13.0	17.0