Search
Logic seminar
С.Н. Васильев: "Автоматическое доказательство и синтез теорем в языке позитивно-образованных формул"
Понедельник, 9 ноября, комната 203. Начало в 14:00.
Докладчик: С. Н. Васильев (Москва, ИПУ РАН).
Тема: Автоматическое доказательство и синтез теорем в языке позитивно-образованных формул.
Abstract
Доклад развивает метод редукции [1], разработанный как аппарат математической теории систем, в частности, для исследования свойств динамических систем и с формально-логической точки зрения являющийся методом решения так называемых согласованных логических уравнений (ЛУ) в языке позитивно-образованных формул (ПО-формул) [1] (первопорядкового типа). Кроме того, используются исчисления ПО-формул [2] (с единственным унарным правилом вывода), а также результаты из [3,4] по алгоритмизации синтеза условий выводимости некоторого подкласса ПО-формул на основе некоторой комбинации стратегии дедукции ПО-формулы, отвечающей исходному ЛУ, с абдукцией - одновременным формированием дополнительной посылки как нового условия для обеспечения выводимости рассматриваемой ПО-формулы.
Благодаря таким особенностям языка и исчисления ПО-формул, как крупноблочность представления и обработки знаний, сохранение эвристической структуры знания, и ряду других, обеспечивается хорошая совместимость логики с эвристиками, используемыми для сокращения комбинаторного пространства или для получения решений в заданном классе формул. Обосновывается целесообразность вводимых эвристик (ограничений на подстановки термов в процессе применения правила вывода и др.) с позиций применения к автоматическому синтезу формулировок математических теорем о качественных свойствах динамических и управляемых систем в терминах преобразований, а также к автоматизации синтеза программно-аппаратных средств с заданными спецификациями. Демонстрируется возможность снятия условия согласованности исходных ЛУ, ограничивавшего класс ЛУ, рассматривавшихся в [1].
______________________________
1. С.Н.Васильев. Метод редукции и качественный анализ динамических систем, I-II // Изв. РАН, сер. Теория и системы управления, 2006, №1, с.21-29; №2, с. 5-17.
2. С.Н.Васильев, А.К.Жерлов, Е.А.Федосов, Б.Е.Федунов. Интеллектное управление динамическими системами //М.: Физматлит, 2000.
3. С.Н.Васильев. Метод синтеза условий выводимости хорновских и некоторых других формул // Сибирский математический журнал, т.38, № 5, 1997, с.1034-1046.
4. С.Н.Васильев, А.С.Коновалов. К автоматизации решения задач: метод дооснащения //Тезисы конференции "Мальцевские чтения", ИМ СО РАН, 2009.
