The calculus of positively constructed formulas, its features, strategies and implementation

Originally, the calculus of positively constructed formulas without function symbols was developed by Russian scientists S.N. Vassilyev and A.K. Zherlov by an evolutionary way in describing and solving of control theory problems. This calculus has features which are important, without loss of generality, for control theory applications. Later investigations shown that the calculus has features providing a good possibility to combine the proof procedure and the problem heuristics. Thus, calculus of positively constructed formulas can be characterized both as machine- and human-oriented. In this paper the calculus of positively constructed formulas with function symbols is considered. We provide the proofs of soundness and completeness for this calculus. Features, strategies, and some prototype prover implementation aspects are presented.