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

摘要：

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

关键词：三值逻辑、不完全Kripke结构、正例、反例、证明系统

所属期刊栏目：23

分类号：TP301.1(计算技术、计算机技术)

资助基金：国家自然科学基金国际合作61061130541;国家"九七三"重点基础研究发展计划项目2011CB302904;核高基重大专项2009ZX010303-001-07;计算机软件新技术国家重点实验室南京大学KFKT2011B26

在线出版日期：2011-12-19（万方平台首次上网日期，不代表论文的发表时间）

页数：共10页

页码：1270-1279