Введение к работе
Акт^альность_темыисследований. В настоящее время широко известно важное значение логических методов для применения вычислительной техники в научных исследованиях^ и решении практически значимых задач. Наиболее известными в этом направлении являются применениялогических методов в практике создания языков программирования, экспертных систем и решении комбинаторных проблем большой сложности.
Универсальность языка логики и универсальность средств решения (вывод), сформулированных на языке логики задач, определяют принципиальное значение логики для решения "плохих" проблем и создания мобильных технологий проектирования-программного обеспечения для различных предметных областей. Понимание универсальности языка логики для математики породило в начале XX века логицизм (Б.Рассел, Д.Гильберт и др.) -направление, пытавшееся уложить всю математику в рамки логики. В настоящее время происходит как бы возрождение логицизма, но не для достижения целей собственно математики, а для приложений з различных областях техники и сферах жизни.
Расширение сфера влияния логики происходит за счет широкого применения экспертных систем (от систем советов домохозяйке до систем поддержки принятия политических решений), которые, как правило, содержат блок вывода. Кроме того, появление коммерческих интегрированных систем логического программирования (типа Турбо-Пролог) включило довольно широкий круг программистов в число людей, использующих логику (хотя и в утилитарной форме). Логические методы успешно применяются для решения комбинаторных проблем большой сложности (подкласс NP-подных задач).что позволило решать практически важные задачи теории расписаний. Например, состав-
лять расписания электричек для Бельгии, расписания полетов и обслуживания техники для компании "йофтгаяза".
Если широко смотреть на данную работу, то ее основу со-стзлягот три взаимосвязанных направления:
I) построение формализма более адекватно отражающего способы доказательства теорем содержательной математики, чем классические логические исчисления*
2} программная реализация построенных методов для решения теоретических и прикладных задач*
3) построение и доказательство существования алгоритмов решения массовых алгоритмических проблем.
Первое направление своим истоком имеет исследования по логике. Построение языка логических исчислений, начатое Дж". Булем, было завершено Г.Фреге. Большая выразительная сила созданного языка исчисления предикатов была подтверждена рядом исследователей - Дж.Пеано (система аксиом арифметики). Е.Цермело (система аксиом теории множеств) и др.
Д.Гильберту и его школе принадлежит создание основного (в современном понимании) логического исчисления, а именно. . исчисяеЯ-НЯ предикатов первого порядка. Это исчисление содержит не только формальный логический язык, но также фактически, задаваемую правилами вывода, полуразрешзющую алгоритмическую процедуру (Д.Гильберт, В.&ккерман [9], Д.Гильберт» П.Бернайс tlOl), которая-принципиально обеспечивает установление выводимости для любого доказуемою утверждения (йо не проявляет признаков положительного или отрицательного ответа на этот вопрос для остальных утверждений). Это наиболее наглядно связывает первое и третье направления диссертации. Отметим, что широко известные методы автоматического' доказательства теорем (АДТ): метод резолюций, обратный метод Mac-лава, алгоритм очевидности, используют полурззрешаюаие про-
цедуры, идущие от соответствующих логических исчислений [14, 25, 361.
Нетрудно видеть, что па языке логик достаточно высоких порядков можно записать любые математические утверждения. Однако это можно сделать уже на языке исчисления предикатов первого порядка, что составляет содержание известного тезиса Гильберта [38].
Тезис Гильберта становится более ясным, если использовать язык многосортного исчисления предикатов для многоосновных моделей. Построение многосортного исчисления -предикатов начато А.Шмидтом, а первые наиболее яркие приложения получены А.И.Мальцевым [19]. Формализм алгебраических систем и расширение многосортного исчисления предикатов с помощью типовых условий для кванторов использовался в работах академика В.М.Матросова и С.Н.Васильева по синтезу теорем о динамических свойствах нелинейных систем [3-7, 26 - 28, 56]. В работах В.М.Матросова и С.Н.Васильева, видимо, впервые были получены на ЭВМ содержательные теоремы (сравнимые с публикуемыми в математических журналах).
Появление вычислительной техники позволило перевести вопрос реализации систем логического вывода и эвристических троцедур проверки истиности (или их комбинации) в практичес-сую плоскость (второе направление работ диссертации). Начало 5ыло положено классической работой А.Ньюэлла, Дж.Шоу и Г. Саймона [53] по созданию эвристической программы для доказательства теорем исчисления высказываний. Дальнейшее продви-<ение связано с открытием Дк.Робинсоном принципа резолюции 36], разработкой С.Ю.Масловым обратного метода [25], рабо-ами по созданию формального языка для записи математических еорий и алгоритма очевидности [ 12 ]. Интенсификация иссле-[ований в данной области связана с появлением языков логи-еского программирования [ 18, 42 ] и экспертных систем.
Исследования в данной области ведутся весьма интенсивно во многих научных центрах Запада, как отдельными учеными, так и довольно большими коллективами. В настоящее время это прежде всего относится к лабораториям, разрабатывающим либо крупные проекты экспертных систем (например, на уровне национальных проектов или для крупных производств), либо создающих интепретаторы (трансляторы) языков логического программирования или системы логического вывода.
Мы не в состоянии привести достаточно полный обзор данного направления из-за недостатка места, но дадим краткий список наиболее интересных (с нашей точки зрения) теоретических и программных разработок, а также проектов, во многом определивших нынешнее состояние дел в этой области и перспективы в обозримом будущем.
-
Программная система "1огик-теоретик",1957г., авторы: А.Ньюзлл, Дж.Шоу и Г.Саймон. Доказательство теорем исчисления высказываний [53].
-
Программные системы "Программа I, II, III", I960, автор: Ван Хао. АДТ исчисления предикатов [57].
-
Обратный метод, 1964, автор С.Ю.Маслов. АДТ исчисления предикатов [25].
-
Программная система "А.ЛПЕБ-ЛОМИ-2", 1965, авторы: Н.А.Шанин, С.Ю.Маслов, Г.В.Давыдов и др. АДТ исчисления высказываний [41, 42].
-
Метод резолюций, 1965, автор: Дж.Робинсон. АДТ исчисления предикатов [36].
6. Программная система "Доказатель Бойера-Мура" и
идеи реализации метода резолюций, 1972, авторы: Р.Бойер,
Дж.Мур. АДТ исчисления предикатов [50].
7. Алгоритм очевидности и программная система САД, 1972, авторы: В.М.Глушков, Ю.В.Капитонова, А.А.Летичевский и др. АДТ исчисления предикатов [ II 1.
8.Программная система "Язык логического программирования ПРОЛОГ', 1973, авторы: А.Колмероэ и др. Язык программирования с решателем задач, описанных хорновскими дизъюнктами [;47].
9. Программная система "Доказатель теорем Техасского
университета", 1974,. авторы: В.Бледсоу, П.Брюэлл и др. АДТ
исчисления предикатов [44, 45].
10. Доклад Р.Ковальского на Конгрессе ІГІР, IS74.
Обоснование логического программирования [50].
11. Программная система: Эдинбургский пролог, 1977,
автор: Д.Уоррен. Язык программирования с решателем задач,
описанных хорновскими дизъюнктами, t 58 ].
12. Метод сравнения и программная система синтеза
теорем, 1978, авторы: С.Н.Васильев, В.М.Матросов и др.
Синтез теорем о динамических свойствах нелинейных
систем [26 - 28].
-
Японский национальный проект. ЭВМ 5-го поколения, 1979,авторы: Т.Мото-ока и др. Системы обработки информации, заключенной в накопленных знаниях, [ 49 ].
-
Программные системы:- AURA " и ША, 1982, авторы: Л.Воз, Э.Ласк и др. АДТ исчисления предикатов и решение прикладных задач, [ 52, 59 ].
-
Проект развития систем логического вывода МККР, 1984, авторы: К.Раф и др. АДТ исчисления предикатов
[ 54 ].
16. Семантическое программирование, 1985, авторы:
С.С.Гончаров, Д.И.Свириденко. Концепция программирования, основанная на формульном описании вычислимых функций [13].
17. Метод удовлетворения ограничениям в логическом программировании и система решения прикладных задач, 1989, авторы: П.ван Хентенрик и др. Методы ориентированные на решение комбинаторных проблем большой сложности 148]. Решение практически важных задач теории -расписаний большой размерности.
2ль_работы. Разработка формализма для моделирования математического-мышления, построение логических исчислений, ориентированнных на создание' систем автоматического доказательства " теорем, проведение исследований по определению свойств построенвых логических исчислений (полнота, область-'конструктивной работы, корректность и др.).
Программная реализация логико-эвристических методов для проведения научных исследований и решения прикладных задач.
Построение и доказательство существования алгоритмов решения массовых алгоритмических проблем.
Метода_исследований. Б работе используются методы математической логики, дискретной метеыатики, теоретической кибернетики, теории моделей и математической теории логического вывода.
" ЭХ55^|0визна.г See основные результаты диссертации, ямшггея новыми и опубликованы в работах автора. В диссертации предлагается новый метод автоматического доказательства теорем ( метод инвариантных преобразований ), отличающийся по своим свойствам {сложность, область конструктивной работы и пр.) от других методов.
Приведены программные реализации метода инвариантных
преобразований (система АВТОЛОТ) и логико-эвристических методов (системы КАРАТІ, КАРАТ2, АВТОР), успешно решающие прикладные и теоретические задачи.
Для двух массовых алгоритмических проблем проведены исследования их разрешимости.
Практетеская_и_теор^тическая_ценность. Метода автоматического доказательства теорем предназначаются для проверки истинности тех или иных классов формул исчисления предикатов, причем эти метода ориентированы на реализацию на ЭВМ (в этом их отличие от классических логических исчислений). Сразу же .отметим, что "универсального" метода- АДТ (проверяющего истинность любых формул исчисления предикатов) нет, так как данная массовая алгоритмическая проблема неразрешима. В силу этого нужен целый спектр методов , имеющих какие-либо преимущества для тех или иных целей.
В диссертации рассматривается, предложенный автором, метод автоматического доказательства теорем . Данный метод, как показал автор и его ученики, имеет ряд преимуществ по сравнению с другими методами на важных классах формул.
. Программная релизация метода (система АВТОДОТ) успешно опробована на решении ряда теоретических и прикладных задач, что подтверждается актом сдачи программной системы межведомственной комиссии и актами внедрения от в/ч 0ІІ68 и в/ч І9ІВІ.
Программные реализации логико-эвристических методов (системы КАРАТІ и КАРАТ2) ориентированы на решения задач распознавания ситуаций в условиях неполной информации и для организации взаимодействия должностных лиц в условиях жестких временных ограничений. Успешная работа данных систем подтверждена справкой от в/ч 0ІІ68.
Программная реализация логико-эвристических методов
система АВТОР для проектирования расписаний вузов успешно работает в Иркутском техническом университете, что подтверждено актом об передаче в опытную эксплуотацию.
Апробация .работы. Результаты диссертации излагались на . vB! Международном конгрессе по логике, философии и методологии науки (Москва, август, 1987), на ряде Всесоюзных конференций по алгебре (І97І-І990г.г.) на всех Всесоюзных и медународных конференциях по прикладной логике (Новосибирск, 1985-1992 г.г., Иркутск, 1995г.>, на VII и Ш Всесоюзных конференциях "Проблемы теоретической кибернетики" (Иркутск, 1985; Горький, 1988), семинарах отделов Ш.СО, АН СССР 1І975 -90 г.г.), Ш РАН (1981-94 г.г.)І'ВЦ АН Арм.ССР (1987 г.), ЛОМИ АН СССР (І980-Г986 г.г.), семинарах МГУЦ982-1989г.г.), кафедры алгебры, логики и кибернетики ИГУ (І972-ГІ995 г.г.), на семинарах КрВЦ СО РАН (1977-1995 г.г.).
Публикации. Основные результаты диссертации опубликованы, в работах tl—151, список которых приводится в конце автореферата.
Структура_и_объем_работы. Диссертация разбита на два тома Первый том состоит из введения и первой главы. Второй том.- -состоит из второй и третьей глав, заключения и списка литература. Введение разбито на 4 параграфа, первая глава -из 5, вторая глава - на 3,"Чретья; -' на '4г-Объем работы' -,293 страницы. Список литературы содержит 181 наименование.
