New Logics for Intelligent Control

New automatic theorem proving (ATP) techniques for application in control systems and artificial intelligence are proposed. New logical first-order languages in descriptive and constructive semantics are considered. These languages consist of 1-st order formulas with type-quantifiers. Logical calculi of classical and intuitionistic types as well as strategies of automated reasoning are defined. Information on results of these logical tools usage in some control problem is given. Keywords: Automatic theorem proving, Descriptive and constructive logics, Intelligent control.