On the calculus of positively constructed formulas for authomated theorem proving

The paper deals with an expressive logic language LF and its calculus. Formulas of this language consist of some large-block structural elements, such as type quantifiers. The language LF contains only two logic symbols — $\forall$ and $\exists$, which form the set of logic connectives of the language. A logic calculus JF and complete strategy for automated proof search based on a single unary rule of inference are considered. This calculus has a number of other features that lead to the reduction of combinatorial complexity of finding the deductions in comparison with the known systems for automated theorem proving as the resolution method and Genzen calculus. Problems of effective implementation of JF as a program system for automated theorem proving are considered.