Введение к работе
Актуальность проблемы.
Задача построения машины, которая могла бы думать так же, как человек, имеет давнюю историю, однако реальное ее решение могло начаться лишь с появлением ЭВМ. Уже в середине 50-х годов появились первые программы,которые могли доказывать теоремы в некоторых областях математики .
Эти программы реализовали известные в то время методы поиска вывода в исчислениях генценовского типа > исчислениях секвенций . Главная трудность в применении этих методов состоит в том, что при контрприменении .кванторных правил необходимо указать значение t переменной X, которое надо подставить, чтобы получить посылки этих правил. Вторая трудность состоит в том, что при контрприменении некоторых прпозицио-нальных правил происходит разветвление процесса поиска с дублированием значительной части информации, что приводит к экспоненциальному росту пространства поиска.
Быстро растущее пространство поиска при использовании таких методов не позволили программам, реализующим эти методы, получить практически значимые результаты.
Практическое использование программ автоматического доказательства теорем пришлось на программы следующего поколения, появившиеся в середине 60-х годов . Новое поколение программ было основано на методах поиска нового типа В 1964г. С.Маслов и Д.Робинсон независимо разработали два новых метода поиска вывода: обратный метод (С.Маслов) и метод резолюций (Д.Робинсон).Новые методы так же, как и их предшественники, использовали идею метаперененных, но в отличие от них были локальными, т.е. согласование значений метаперененных происходило по мере надобности при применении каждого' правила вы-
вода.Другим существенным отличием этих методов от прежних бы ло то, что поиск вывода в них осуществлялся в направлении "сверху-вниз". Важным преимуществом методов являлась их эв-ристичность, направленность на поиск вывода, именно заданной формулы. Главная идея обоих методов состоит в том, что по за данной формуле строится специальное исчисление (исчисление дизъюнктов для метода резолюций и исчисление благоприятных наборов для обратного метода),и поиск вывода происходит в этом исчислении по весьма простым локальным правилам вывода. Новые методы получили название методов резолюционного тип или локальных .
В настоящее время известно довольно много действующих систем, в которых реализованы локальные методы поиска вывода
Области использования-таких систем весьма разнообразны. В первую очередь это различные разделы математики:алгебра , геометрия , математический анализ , математическая логика. Имеется ряд систем, используемых в проектировании , автоматизированном обучении , решении проблем . Отдельно можно упс мянуть об использовании локальных методов в экспертных сист< мах . Наконец, широкое поле применений представляет программирование: верификация программ, синтез программ .
Особенно большое внимание уделяется в последнее время синтезу программ на основе методов математической логики .
Центральную роль в синтезе программ играют системы авті матического поиска доказательств, и исследование и разработ: таких систем - весьма актуальная и важная проблема.
Таким образом, актуальность исследования связывается с
использованием локальных методов поиска вывода в качестве а
парата теоретических исследований алгоритмических проблем м
тематики и как.средства построения интеллектуальных систем
для решения прикладных задач в различных предметных областях.
Цель работы.
. - разработка техники доказательства полноты стратегий поиска для локальных методов;
расширение сферы применения локальных методов на различные, в том числе и на неклассические, логики;
разработка техники доказательства разрешимости различных классов формул и построение разрешающих алгоритмов на базе локальных методов поиска;
разработка логических основ системы логического вывода, ориентированной на решение прикладных задач из разных предметных областей.
Методы исследования.
В работе используются идеи, понятия и методы теории доказательств, теории и практики дедуктивного синтеза программ.
Научная новизна работы.
На основе предложенного автором понятия двойственной стратегии сформулированы определения и доказана полнота некоторых стратегий для метода резолюций. Предложенная автором :тратегия поиска оказалась весьма эффективной для поиска до-сазательств формул логики предикатов и оказалась разрешающей і;ля целого ряда разрешимых классов. Автором предложен вариант іетода резолюций для нескулемизированных формул, идеи которо-о позволили ему построить локальные методы резолюционного ипа для модальных логик. Для построенных таким образом мето-
дов оказались полными все стратегии поиска вывода , известные для классической логики предикатов. Одна из таких стратегий оказалась разрешающей для модальных пропозициональных логик S4 и S5. Разработанная под научный.руководством автора система логического программирования СИНТЕЗ оказалась удобным средством для решения технологических задач и используется не ряде предприятий в качестве ядра экспертных систем в различных предметных областях.
Практическая полезность работы.
Разработанные автором стратегии поиска были реализованы на ЭВМ и показали высокую эффективность. Предложенные методы поиска для классической логики предикатов и модальных логик позволяют решать теоретические задачи математической логики J программирования. Система логического программирования СИНТЕЗ, разработанная под руководством автора, позволяет решать прикладные задачи в различных предметных областях.
Апробация работы.
Основные результаты работы были доложены на научных семинарах в ИК АН Эстонии, (г. Таллинн - 1989г.), ИМ СОАН СССР (г. Новосибирск - 1989г.), ИТА АН СССР (г.Ленинград -1985г.), на рабочей группе по представлению знаний и эксперт ним системам при НТС по информатике и вычислительной технике межведомственного координационного совета АН СССР (г. Ленинг рад - 1985г.), на Всесоюзной конференции по математической ' логике (г. Новосибирск - 1974г.), Всесоюзных семинарах "Семи отические аспекты формализации интеллектуальной деятельности
(г.Кутаиси - 1985г., г.Боржоми - 1988г.), Всесоюзной конфе-
' - 6 -
ренции по прикладной логике (г.Новосибирск - 1985г.), Международной конференции FCT-87 (г. Казань - 1987г.).
Публикации.
Основные результаты диссертации опубликованы в 8 работах, перечисленных в списке литературы. Из совместных работ в диссертацию включены лишь результаты, полученные лично автором.
Объем и структура диссертации.
