G_3逻辑中的弱合取范式  

Weak Conjunctive Normal Form for G_3 Logic

作　　者：章衡[1] 张明义[2] 杨本娟[1] 

机构地区：[1]贵州大学信息工程学院 [2]贵州科学院,贵阳550002

出　　处：《计算机科学》2007年第4期158-162,共5页Computer Science

基　　金：国家自然科学基金(60573009);贵州省长基金2005(212)资助

摘　　要：本文为G3逻辑提出一种类似于经典逻辑中合取范式的弱合取范式,并给出两种范式化简算法:一种是通过公式刻画反模型的语义方法;另一种为基于重写翻译的语法方法。文章最后证明,在G3逻辑中对任意公式做弱合取范式化简不存在多项式算法。In this paper, we put forward a weak conjunctive normal form for G3 logic, which is similar to the conjunctive normal form for classical propositional logic. We also give two algorithms to reduce a formula to the weak, conjunctive normal form, where one is based on eharaetering counter models in model-based-formulas, and the other is based on rewriting formulas according to transformation rules. In the end, we show that there is no polynomial time algorithm to reduce an arbitrary formula to the weak conjunctive normal form.

关 键 词：弱合取范式 G3逻辑 范式化简 计算复杂性 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]