On a method of solution the equality problem for positively constructed formulas

The calculus of positively constructed formulas (PCF) is a first-order formalism that has many features useful for solving problems of dynamic systems control. This formalism is used as a basis for automatic theorem proving (ATP) systems. Many problems in the field of ATP can be formalized only with the use of equality predicate. Using this predicate will require adding extra axioms into the problem. This is not efficient for ATP systems, so the problem of equality must be solved without that axioms. In this paper, we introduce the solution of equality problem for PCF formalism. The results are integrated into the developed ATP system.