Доклад развивает метод редукции, разработанный как аппарат математической теории систем, в частности, для исследования свойств динамических систем и с формально-логической точки зрения являющийся методом решения так называемых согласованных логических уравнений (ЛУ) в языке позитивно-образованных формул (ПО-формул) (первопорядкового типа). Кроме того, используются исчисления ПО-формул (с единственным унарным правилом вывода), а также результаты из по алгоритмизации синтеза условий выводимости некоторого подкласса ПО-формул на основе некоторой комбинации стратегии дедукции ПО-формулы, отвечающей исходному ЛУ, с абдукцией - одновременным формированием дополнительной посылки как нового условия для обеспечения выводимости рассматриваемой ПО-формулы.
Благодаря таким особенностям языка и исчисления ПО-формул, как крупноблочность представления и обработки знаний, сохранение эвристической структуры знания, и ряду других, обеспечивается хорошая совместимость логики с эвристиками, используемыми для сокращения комбинаторного пространства или для получения решений в заданном классе формул. Обосновывается целесообразность вводимых эвристик (ограничений на подстановки термов в процессе применения правила вывода и др.) с позиций применения к автоматическому синтезу формулировок математических теорем о качественных свойствах динамических и управляемых систем в терминах преобразований, а также к автоматизации синтеза программно-аппаратных средств с заданными спецификациями. Демонстрируется возможность снятия условия согласованности исходных ЛУ, ограничивавшего класс ЛУ.
