Positive constructed formulas preprocessing for automatic deduction

The preprocessing of positively-constructed formulas (PCFs) for automatic deduction search algorithms is considered in this paper. A new efficient algorithm for conversion of the predicate calculus language formulas to the language of PCFs and equivalent rules of reducing PCFs, preserving the original heuristic structure of knowledge represented by the formulas of the predicate calculus language, are presented.