摘要
本文为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.
出处
《计算机科学》
CSCD
北大核心
2007年第4期158-162,共5页
Computer Science
基金
国家自然科学基金(60573009)
贵州省长基金2005(212)资助
关键词
弱合取范式
G3逻辑
范式化简
计算复杂性
Weak conjunctive normal form, G3 logic, Normal form reduction, Computational complexity
