Введение к работе
Актуальность темы. Проблемы автоматизации доказательства теорем и порождения гипотез (синтеза теорем) являются фундаментальными проблемами в области математической логики и искусственного интеллекта. Изучение приемов доказательства теорем сыграло большую роль в развитии методов искусственного интеллекта. Формализация де-дуктизного процесса с использованием языка логики предикатов помогает глубже понять некоторые компоненты рассуждения. Многие неформальные задачи допускают их формализацию как задачу на доказательство теорем. Поэтому компьютерная логика важна.
Менее традиционной считается проблематика машинного синтеза теорем, хотя она имеет также давнюю историю как и задачи автоматического доказательства теорем. Еще X. Вонг (Wang Н.)1 и В.М. Глушков2 отмечали не меньшую значимость, хотя и большую трудность задачи автоматизации получения самих формулировок теорем.
Подходы к автоматизации синтеза теорем условно можно разбить на четыре направления: дедуктивное развертывание теории, припцилы саморазвития теории, корректирование недоказуемых гипотез, алгоритми-зационный подход.
Развертывание теории па основе ограничиваемого вывода впервые было апробировано на ЭВМ X. Вонгом в рамках секвенциального исчисления высказываний. В.М. Глушковым были предложены общие принципы саморазвития теории. Несколько промежуточное положение между задачами синтеза и доказательства теорем занимает задача корректирования недоказуемых гипотез. Подход к ее решению в исчислении высказываний предложен Г.В. Давыдовым.
Эффективным подходом к автоматизации синтеза и доказательства теорем в хорошо разработанных узких областях математических теорий является алгоритмизацнонный подход. Он основан на анализе техники формулировок и доказательств известных теорем рассматриваемой области. Основными достоинствами подхода являются меньшая комби-наторность вывода и большая понятность промежуточных результатов человеку по сравнению с ранее рассмотренными подходами. С использованием такого подхода В.М. Матросовым в динамике систем был пред-
1Воаг X. На пути к механической математике // Киберн. сб.-1962.-Т.5.- С.114-165. 2Глушков В.М. Машина доказывает. -М.: Знание, 1981. -64 с.
ложен принцип сравнения с вектор-функциями Ляпунова. Этот принцип определил алгоритм вывода теорем с вектор-функцаями Ляпунова для широкого класса динамических свойств систем процессов. Развитый С.Н. Васильевым подход к алгоритмизации синтеза теорем на основе решения логических уравнений в исчислении предикатов первого порядка с типовыми кванторами показал важность исследования новых классов логических уравнений, дающих содержательные результаты. Практическое использование результатов алгоритмического подхода, как и компьютерной логике, вообще, нуждается в разработке математического программного обеспечения.
Цель работы. Настоящая работа преследует следующие основные цели: дальнейшее развитие алгоритмов метода синтеза теорем на основе решения логических уравнений в дескриптивной семантике; создание метода решения логических уравнений в конструктивной семантике; создание программной системы, реализующей алгоритмы решения логических уравнений в исчислении предикатов первого порядка; приложение методов решения логических уравнений в различных предметных областях.
Методика исследований. Общая методика исследований состоит в применении современных методов математической логики и теории программирования.
Научная новизна. Результаты диссертации являются новыми.
Разработан новый алгоритм для согласования логических уравнений в дескриптивной семантике.
Предложен алгоритм построения формул связи в анализе управляемых систем.
Разработан метод решения логических уравнений в конструктивной семантике.
Создана система автоматического синтеза теорем (ACT) для ПЭВМ класса IBM AT.
Предложенные алгоритмы и средства апробированы в задачах исследования свойств управляемых систем, анализа синтезируемости логических структур СБИС, распознавания типа летательных аппаратов, анализа технологических процессов.
Практическая значимость полученных результатов: Полученные результаты позволяют существенно расширить область применения методов синтеза теорем. Алгоритмы согласования логических уравнений позволяют расширить область применимости метода синтеза теорем в ма-
тематической теории систем. Алгоритмическое построение формул связи полезно для повышения степени автоматизированного синтеза теорем о динамических свойствах управляемых систем. Метод синтеза теорем в конструктивной семантике является хорошим инструментом в задачах планирования действий (вычислений и т.п.) Использование системы ACT позволяет существенно сократить время, затрачиваемое высококвалифицированными специалистами на получение формулировок теорем, а также повысить уровень интеллектуальности автоматических и автоматизированных систем в условиях неполноты информации и/или ограниченности ресурсов.
Апробация работы. Результаты диссертационной работы докладывались на Школах по пакетам прикладных программ (Иркутск, 1989, Адлер 1991), на Всесоюзных конференциях по прикладной логике (Новосибирск, 1985, 1988, 1992), на научной школе "Автоматизаціїя создания математического обеспечения и архитектуры систем реального времени" (Иркутск, 1990), на Республиканском научно-техпическом семинаре "Машинные методы в задачах механики, устойчивости и управления" (Казань, 1990), на Всесоюзной научно-технической конференции "Интеллектуальные системы в машиностроении" (Самара, 1991), на Республиканской конференции "Современные проблемы алгоритмизации" (Ташкент, 1991), на Международном семинаре "Методы и программное обеспечение для автоматических управляемых систем" (Иркутск, 1991), на Всероссийской научной школе "Компьютерная логика, алгебра и иятеллектное управление" (Иркутск, 1994).
Публикации. Основные результаты диссертации опубликовапы в 13 печатных работах.
Структура и объем работы. Диссертационная работа состоит из введения, трех глав, заключения, списка литературы и приложения. Список литературы содержит 100 наименований. Основной текст работы изложен на 135 страницах машинописного текста.
