Program for converting formulas of the first-order predicate calculus into a conjunctive normal form. Implementation based on a binary tree.
Преобразование формул исчисления предикатов первого порядка в конъюнктивную нормальную форму. Реализация на основе бинарного дерева.