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

Proof System of 3-valued Logic and the Finding of Witness and Counterexample

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

3-valued logic model checking is suitable for the reasoning based on higher-level abstract model.However,for 3-valued model checking algorithm,the witness and counterexample needs to be found.Therefore,3-valued model checking technology and the finding of witness and counterexample are explored in this paper.A set of 3-valued logic rules is proposed and a proof system is formed.This can be used to prove whether a model satisfies a property.The witness（counterexample） can be found for an existential（a universal） path quantifier during the proving procedure.The direction of a model refinement can be given by the achievement of witness and counterexample.Finally an example is given to explain the application of this proof system in the verification of digital logic designing.