CNF Transformation Calculus A Calculus CNF0 withe the following Inference Rules on sets of Labeled Formula: