|
计算机科学 2007
Weak Conjunctive Normal Form for G3 Logic
|
Abstract:
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 charactering 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.