三值逻辑证明系统及正例与反例的提取

• 作者: 郭建 韩俊刚
• 来源期刊: 计算机辅助设计与图形学学报
• 学科: 工学
• 关键词: 三值逻辑 不完全Kripke结构 正例 反例 证明系统
• 年，卷（期）: 2011,（7）
• 所属期刊栏目: VLSI设计与测试及电子设计自动化
• 页码范围: 1270-1279
• 分类号: TP301.1
• 字数: 9303字
• 语种: 中文

摘要

三值逻辑模型检验是对更高层的模型抽象验证的一种方法,对其验证中常常需要给出正例和反例.为此,讨论了三值逻辑模型检验以及正例和反例的提取,并在给出一套三值逻辑证明规则的基础上形成一个证明系统;运用该系统可以证明模型是否满足某个性质;在证明过程中为存在路径量词提取正例,为全称路径量词提取反例.正例和反例的提取可给模型的细化指明方向.最后通过实例给出了该证明系统在数字逻辑电路验证中的应用.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	韩俊刚	西安邮电学院计算机科学系	113	703	14.0	20.0
2	郭建	华东师范大学软件学院	5	11	2.0	3.0