Описываются логические средства автоматического доказательства и синтеза теорем, которые отличаются от известных своими выразительными, дедуктивными и абдуктивными возможностями. Положительная апробация осуществлена в проблематике интеллектного управления динамическими системами и автоматического синтеза теорем математической теории систем.