Indexing 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. For investigation of this formalism, analysis of logical inference of formulas is used. The logical inference consist of many PCF. The analysis of big amount of formulas require special operations: search of formulas, search by template, unification search etc. Usually for solving these problems the indexing methods are used. For indexing terms as a tree-like structures the methods of indexing such as path indexing, substitution tree indexing, discrimination tree indexing etc., are used. This methods well used in many logical systems. Since PCF, like a term, have a tree-like structure, the generalization of indexing methods to the PCF indexing is possible. In this paper, we consider this problem. The modification of indexing methods and experiments concerning the analysis of logical inferences (big sets of PCF) are presented.