On the calculus of positively constructed formulas for authomated theorem proving

Abstract

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 quanti¯ers. The language LF contains only two logic symbols for any and is, 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 ¯nding 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.

Keywords

• automated theorem proving
• mathematical logic
• nonclassical logics
• artificial intelligence