An Algorithm for Weak Disjunctive Normal Form Reduction in G3 Logic

In this paper, we put forward a weak conjunctive normal form for G3, which is similar to the conjunctive normal form for classical propositional logic. We also give two algorithms to reduce a formula to weak conjunctive normal form, where one is based on charactering countermodels 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.