автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.16, диссертация на тему:Локальные методы поиска вывода в автоматическом решении задач

ж ¿бгуо? ^^ /

// // ¿-5 АКАДЕМИЯ НАУК СССР ' °

ЛЕНИНГРАДСКИЙ ИНСТИТУТ ИНФОРМАТИКИ И АВТОМАТИЗАЦИИ

На правах рукописи

ЗАМОВ Наиль Калимович

УДК 519. 68:159.955

ЛОКАЛЬНЫЕ МЕТОДЫ ПОИСКА ВЫВОДА В АВТОМАТИЧЕСКОМ РЕШЕНИИ ЗАДАЧ

05.13. 16 - применение вычислительной техники, математического моделирования и математических методов в научных исследованиях

Автореферат

диссертации на соискание ученой степени доктора физико-математических наук

ЛЕНИНГРАД - 1989

? о . ' ,

м ; с /

Работа выполнена в Казанской государственном университете Официальные оппоненты:

доктор физико-математических наук АРТЕМОВ С.Н.

доктор физико-математических наук профессор ГОНЧАРОВ С.С. доктор технических наук

Институт кибернетики Академии наук Эстонии

ГОРОДЕЦКИЙ В.И.

Ведущая организация:

Защита состоится ".

1990 г. в ... часов

на заседании Специализированного совета Д.003.62.01 при Ленинградском институте информатики и автоматизации АН СССР по адресу : 199178, г. Ленинград, 14-я линия, д. 39.

С диссертацией можно ознакомиться в научной библиотеке Специализированного совета Д.003.62.01.

Автореферат разослан

Ученый секретарь Специализированного совета, доктор технических наук

Домарацкий А. 11.

Актуальность проблемы.

Задача построения машины, которая могла бы думать так же, как человек, имеет давнюю историю, однако реальное ее решение могло начаться лишь с появлением ЭВМ. Уже в середине 50-х годов появились первые программы,которые могли доказывать теоремы в некоторых областях математики .

Эти программы реализовали известные в то время методы поиска вывода в исчислениях генценовского типа исчислениях секвенций . Главная трудность в применении этих методов состоит в том, что при контрприменении .кванторных правил необходимо указать значение 1 переменной X, которое надо подставить, чтобы получить посылки этих правил. Вторая трудность состоит в том, что при контрприменении некоторых прпозицио-нальных правил происходит разветвление процесса поиска с дублированием значительной части информации, что приводит к экспоненциальному росту пространства поиска.

Быстро растущее пространство поиска при использовании таких методов не позволили программам, реализующим эти методы, получить практически значимые результаты.

Практическое использование программ автоматического доказательства теорем пришлось на программы следующего поколения, появившиеся в середине 60-х годов . Новое поколение программ было основано на методах поиска нового типа В 1964г. С.Маслов и Д.Робинсон независимо разработали два новых метода поиска вывода: обратный метод (С.Маслов) и метод резолюций (Д.Робинсон).Новые методы так же, как и их предшественники, использовали идею метапеременных, но в отличие от них были локальными, т.е. согласование значений метапеременных происходило по мере надобности при применении каждого' правила вы-

3

вода.Другим существенный отличней этих методов от прежних бы ло то, что поиск вывода в них осуществлялся в направлении "сверху-вниз". Важным преимуществом методов являлась их эв-ристичность, направленность на поиск вывода, именно заданной формулы. Главная идея обоих методов состоит в том, что по за данной формуле строится специальное исчисление (исчисление дизъюнктов для метода резолюций и исчисление благоприятных наборов для обратного метода),и поиск вывода происходит в этом исчислении по весьма простым локальным правилам вывода. Новые методы получили название методов революционного тип или локальных .

В настоящее время известно довольно много действующих систем, в которых реализованы локальные методы поиска вывода

Области использования-таких систем весьма разнообразны. В первую очередь это различные разделы математики:алгебра , геометрия , математический анализ , математическая логика. Имеется ряд систем, используемых в проектировании , автоматизированном обучении , решении проблем . Отдельно можно упс мянуть об использовании локальных методов в экспертных сист* мах . Наконец, широкое поле применений представляет программирование: верификация программ, синтез программ .

Особенно большое внимание уделяется в последнее время синтезу программ на основе методов математической логики .

Центральную роль в синтезе программ играют системы авт! матического поиска доказательств, и исследование и разработ: таких систем - весьма актуальная и важная проблема.

Таким образом, актуальность исследования связывается с использованием локальных методов поиска вывода в качестве а парата теоретических исследований алгоритмических проблем м тематики и как.средства построения интеллектуальных систем

- 4 -

для решения прикладных задач в различных предметных областях.

Цель работы.

. - разработка техники доказательства полноты стратегий поиска для локальных методов;

- расширение сферы применения локальных методов на различные, в том числе и на неклассические, логики;

- разработка техники доказательства разрешимости различных классов формул и построение разрешающих алгоритмов на базе локальных методов поиска;

- разработка логических основ системы логического вывода, ориентированной на решение прикладных задач из разных предметных областей.

Методы исследования.

В работе используются идеи, понятия и методы теории доказательств, теории и практики дедуктивного синтеза программ.

Научная новизна работы.

На основе предложенного автором понятия двойственной стратегии сформулированы определения и доказана полнота некоторых стратегий для метода резолюций. Предложенная автором ¡тратегия поиска оказалась весьма эффективной для поиска до-сазательств формул логики предикатов и оказалась разрешающей ;ля целого ряда разрешимых классов. Автором предложен вариант 1етода резолюций для нескулемизированных формул, идеи которо-•о позволили ему построить локальные методы резолюционного ■ипа для модальных логик. Для построенных таким образом мето-

- 5 -

дов оказались полными все стратегии поиска вывода , известные для классической логики предикатов. Одна из таких стратегий оказалась разрешающей для модальных пропозициональных логик

Разработанная под научный.руководством автора система логического программирования СИНТЕЗ оказалась удобным средством для решения технологических задач и используется не ряде предприятий в качестве ядра экспертных систем в различных предметных областях.

Практическая полезность работы.

Разработанные автором стратегии поиска были реализованы на ЭВМ и показали высокую эффективность. Предложенные методы поиска для классической логики предикатов и модальных логик позволяют решать теоретические задачи математической логики ] программирования. Система логического программирования СИНТЕЗ, разработанная под руководством автора, позволяет решать прикладные задачи в различных предметных областях.

Апробация работы.

Основные результаты работы были доложены на научных семинарах в ИК АН Эстонии, (г. Таллинн - 1989г.), ИМ СОАН СССР (г. Новосибирск - 1989г.), ИТА АН СССР (г.Ленинград -1985г.), на рабочей группе по представлению знаний и эксперт ним системам при НТС по информатике и вычислительной технике межведомственного координационного совета АН СССР (г. Ленинг рад - 1985г.), на Всесоюзной конференции по математической ' логике (г. Новосибирск - 1974г.), Всесоюзных сеиинарах "Семи отические аспекты формализации интеллектуальной деятельности

(г.Кутаиси - 1985г., г.Боржоми - 1988г.), Всесоюзной конфе-

' - 6 -

ренции по прикладной логике (г.Новосибирск - 1985г.), Международной конференции гст -87 (г. Казань - 1987г.).

Публикации.

Основные результаты диссертации опубликованы в 8 работах, перечисленных в списке литературы. Из совместных работ в диссертацию включены лишь результаты, полученные лично автором.

Объем и структура диссертации.

Диссертация состоит из введения и пяти глав, общий объем-составляет 147 страниц. Список литературы состоит из 96 наименований .

Содержание работы.

Введение. Здесь дается краткий обзор достижений в области автоматического доказательства теорем, обосновывается актуальность темы исследования, определено место результатов, представленных в диссертации, в кругу исследований по использованию методов теории доказательств в автоматическом решении задач.

Одним из главных математических результатов, сделавших возможным реальное использование методов автоматического до-<азательства теорем, является появление локальных методов по-*ска вывода. Локальные методы были одновременно и независимо юлучены С.Ю.Масловым в СССР и Д.А.Робинсоном в США и пред-1азначались для поиска вывода в классическом исчислении пре-щкатов.

Локальные методы обладают целый рядом особенностей, которые выгодно отличают их от ранее известных методов .Эти особенности стали предметом глубоких исследований, которые имели целью внести усовершенствования в локальные методы и распространить их не только на классическое исчисление предикатов, но и на другие логики. Среди этих особенностей выделим четыре главные, которые и позволили программам, реализующим эти методы, получить практически значимые результаты:

О) использование языка дизъюнктов для представления формул;

6) наличие единственного, весьма простого, правила вывода

С) использование метапеременных, значения которых уточняются при применении правил вывода;

(1) возможность использования гибких стратегий поиска вывода .

Исследованию этих особенностей и их программным реализациям были посвящены исследования в области автоматического доказательства теорем с середины 60-х годов по настоящее время.

Локальные методы оказались весьма эффективным теоретическим инструментом для построения на их базе разрешающих алгоритмов в некоторых разрешимых теориях и для получения новых разрешимых классов и классов сведения. Так, С.Маслов построил разрешающий алгоритм для широкого класса формул,который содержал в себе почти все известные разрешимые классы исчисления предикатов. Главная идея доказательства разрешимости состояла в тон, что, применяя некоторую полную стратегию" поиска к формулам этого класса, можно вывести лишь конечное число новых объектов.

Предложенный С.Масловым способ доказательства разреши- 8 -

мости был развит и использован для получения разрешающих алгоритмов в других логических исчислениях революционного типа. Исследования в этой области представляют не только теоретический, но и практический интерес, т. к. 'решение .реальных прикладных задач происходит, как правило, в рамках разрешимых теорий .

В настоящее время известно много действующих систем, в . которых реализованы локальные методы поиска вывода. Из зарубежных систем можно выделить универсальные системы AURA , ИР, на которых решались задачи из различных разделов математики. Из отечественных систем автоматического доказательства отметим системы, разработанные в ЛОМИ АН СССР (г.Ленинград), в ИК АН УССР (г.{(иев), в ИТА АН СССР (г.Ленинград) - система СПОРА,, в ИК АН Эстонии (г. Таллинн) -'система ПРИЗ и система для доказательства теорем в исчислении предикатов , в КГУ (г. Казань) - система доказательства теорем для модальных логик.

Известен целый ряд прикладных систем, в которых реализо- ' ваны локальные методы. В первую очередь к ним можно отнести уже упомянутую систему ПРИЗ, которая предназначена для решения вычислительных задач.Система PROLOG используется в качестве системы программирования для решения практически любых задач, входной язык системы стал одним из универсальных языков программирования. Система СИНТЕЗ, разработанная в КГУ (г.Казань) под руководством автора диссертации, используется для автоматического решения технологических задач. Система МАВР , разработанная в ВЦ АН СССР (г.Москва), используется в качестве экспертной системы. Система M0L0G является расширением PROLOG'S средствами модальной логики и используется для формализации логики знаний в базах знаний.

Области использования программ с автоматическим доказа-

- 9 -

тельствоы теореи весьма разнообразны. В первую очередь это различные разделы математики:алгебра , геометрия , математический анализ .математическая .логика. Имеется ряд систем, используемых в проектировании, автоматизированном обучении, решении проблем . Отдельно можно упомянуть об использовании локальных методов в экспертных системах. Наконец, широкое поле применений представляет программирование:верификация программ, синтез программ. Особенно большое внимание уделяется в последнее время синтезу программ на основе методов математической логики .

В области автоматизации поиска вывода , в теории и практике использования локальных методов автором получен ряд новых результатов, которые легли в основу диссертации.

Глава I. Эта глава содержит, в основном, справочный материал. Здесь вводятся определения терминов, понятий. Ставится задача поиска вывода формулы в исчислении предикатов, делается ее редукция к задаче поиска вывода специального объекта в специальном исчислении. Определены методы поиска вывода в этом идчислении, стратегии поиска, методы доказательства полноты стратегий. Материал главы составляют как известные результаты, полученные в разное время разными исследователями, так и результаты, установленные автором диссертации.

Традиционно задача доказательства теорем в некоторой формальной системе Б ставится так: из совокупности аксиом А , применяя правила вывода формальной системы Б, построить вывод теоремы Т. Для большинства теорий, основанных на классической логике,эта задача сводится к следующей: из аксиом А и отрицания ~1 Т теоремы вывести противоречие по правилам И .Таким образом,задача доказательства теоремы Т сводится к задаче

- 10 -

'становления противоречивости совокупности формул А I) {ТТ}.

Традиционная схема решения последней задачи состоит в юпытке доказать выполнимость (неопровержимость) множества формул путем построения модели, в которой аксиомй из А и фор-|ула "1 Т были бы истинными. Удачное завершение этой попытки >значает невыводимость теоремы из множества аксиом, .а неудача )значает, что теорема доказуема.

Попытки построения модели могут быть оформлены в виде [екоторой синтаксической процедуры. Методы, основанные на ис-шслении секвенций и на семантических таблицах , оказались ^эффективными. Эти методы предполагают построение специальна исчислений, в которых для любой формулы строится неболь-юе число ее "предшественников", т.е. формул, из которых она южет быть получена одним применением правила вывода. Процесс [оиска вывода в таком исчислении называют поиском "сни-|у-вверх". Главная трудность при поиске "снизу-вверх" состоит ! том, что для предшественников кванторных формул вида </зГ(Х) или ЗЗСрСО необходимо указать конкретные значения 1еременной I . Если в формуле много кванторов, то требуется :огласовать значения переменных, связанных этими кванторами, (ля такого согласования используется аппарат метапеременных, [редложенный С.Кангером и независимо Д.Правитцем и Н.А.Шани-[ым. При использовании метапеременных в процедуре поиска снизу-вверх" вначале строится некоторая заготовка вывода,в :оторой вместо кванторных переменных используются метапере-1енные, затем производятся согласования значений метаперемен-[ых. Обычно с ростом длины вывода увеличивается размер заго-■овки и увеличивается сложность согласования, что приводит к [еэфективности алгоритма поиска.

Получить более эффективные алгоритмы поиска позволила

- II -

идея организации поиска в направлении "сверху-вниз". При' такой схеме поиска согласование значений нетапеременных происходит не для всей заготовки вывода, а лишь для той ее части, к которой применяется правило вывода. Методы, основанные на идее поиска "сверху-вниз" и локальном согласовании значений метапеременных, были названы С.Масловым локальными методами поиска . К локальным методам относятся обратный метод , метод резолюций и их многочисленные модификции и конкретизации. Прсктически все работающие системы, использующие автоматическое доказательство теорем, реализуют какой-либо локальный ме-•тод поиска.

Теоретической основой всех известных методов доказательства теорем в исчислении предикатов является теорема Эрбрана Теорема Эрбрана позволяет'свести задачу поиска опровержения предикатной формулы к задаче поиска опровержения некоторой пропозициональной формулы. Использование теоремы Эрбрана предполагает реализацию какого-нибудь механизма "угадывания" значений переменных, при которых получается противоречие. Этот механизм реализован в методе резолюций в виде алгоритма унификации, который по заданному множеству выражений строит .требуемую подстановку значений переменных.

Один из подходов к доказательству невыполнимости формул А состоит в построении и анализе дерева всех ее зрбрановских интерпретаций.

Дерево интерпретаций формулы А, в котором каждая ветвь длины К для. некоторого К задает опровержение формулы А, назы вается замкнутым деревом.

Метод резолюций и обратный метод - это, по существу,методы построения замкнутых деревьев для заданной формулы А. Оба метода характеризуются тем, что построение замкнутых де-

- 12 -

ревьев производится в направлении от концевых вершин к корню, однако способы построения деревьев в обоих методах различны.

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

Как следует из теоремы Эрбрана,формула А невыполнима тогда и только тогда, когда невыполнима формула вида А1 ... бА„. где А1 (I < I < П) получено из А подстановкой термов , построенных из скулемовских функций, вместо переменных.

Локальность метода резолюций и обратного метода позволя-. ет строить эти подстановки не сразу в окончательном виде, а постепенно.Существенной частью этих методов является алгоритм построения требуеыых подстановок, который был предложен Робинсоном и называется алгоритмом унификации.

Оба метода построены по одинаковой схеме: по заданной формуле строятся исчисления, выводимые объекты которых связаны с деревом интерпретаций данной формулы. Аксиомами метода резолюций являются дизъюнкты формулы (т.е. сомножители ее к.н.ф.), а аксиомами обратного метода - контрарные пары из литер формулы.

Правило вывода метода резолюций имеет вид

АУ Кь 1ВУ К2 <К»У К2)б

где б - подстановка, унифицирующая отрезаемые литеры А и В..

Правйло вывода обратного иетода ииеет вид*

А,и К,.....А„11 К„

(К»и ... Ц Кп)б _

13

где отрезаемые литеры после подстановки 6. образуют подстанов ковый частный случай некоторого дизъюнкта заданной формулы .

Г.Давыдов, обобщив оба этих метода, предложил общую схему поиска вывода, частными случаями которой являются обратный метод и метод резолюций . Эта схема была развита в работах В.Шаронова и автора диссертации . В результате такого общего подхода появилась возможность унифицировать рассмотрение обоих методов и интерпретировать некоторые результаты, полученные для одного из них, в другом. При подходящем выборе аксиом и отрезаемых литер можно добиться значительного эффекта при поиске вывода .

Далее в работе показаны методы перестроения выводов в обратном методе в выводы в методе резолюций и обратно и дальнейшее изложение ведется в'терминах метода резолюций.

Одним из недостатков использования правила резолюции является его широкая применимость, что приводит к существованию множества различных выводов одного и того же дизъюнкта, кроме того, могут выводиться частные случаи уже выведенных дизъюнктов, а также дизъюнкты, которые не войдут затем по каким-либо причинам"в вывод искомого (пустого) дизъюнкта.

Для того, чтобы ограничить порождение "бесполезных" дизъюнктов, используются различные ограничительные стратегии поиска . Одним из важных требований к стратегиям является требование полноты, т.е. стратегия должна гарантировать построение вывода пустого дизъюнкта для невыполнимого множества дизъюнктов. Для доказательства полноты чаще всего используются следующие два метода. Первый состоит в доказательстве полноты для пропозиционального случая с последующим применением леммы о подъеме. При использовании этого метода, очевидно, требуется, чтобы ограничения, накладываемые стратегией, сохранялись

- 14 -

при подъеме. Доказательство полноты для пропозиционального случая, как правило, проводится индукцией по сложности формулы, обычно - по количеству пропозициональных переменных, по количеству вхождений символов и т.д.

Автором совместно с В.Шароновым была предложена общая схема доказательства полноты различных стратегий. Практически для всех известных в настоящее время стратегий полнота может' быть доказана по этой схеме. Кроме того, предложенная схема позволяет определить совместимость стратегий.

Другой способ доказательства полноты стратегий - перестроение выводов. При этом вывод в каком-либо исчислении (не обязательно резолюционном) перестраивается в революционный вывод с требуемыми свойствами. Таким образом были получены доказательства полноты для стратегий в модальных логиках, стратегий с ограничением факторизации,стратегии линейного вывода . Этот метод был использован автором для получения . "двойственных" стратегий метода резолюций .

Далее обсуждается механизм получения "двойственных" стратегий. Допустим, что мы имеем определение некоторой стратегии метода резолюций. Если мы возьмем произвольный вывод, удовлетворяющий этой стратегии, и перестроим его методом, описанным в работе, то получим некоторый вывод в обратной методе, удовлетворяющий требованиям какой-то стратегии обратного метода. Такую стратегию и будем называть двойственной.

Далее в работе рассматриваются некоторые примеры переноса стратегий из одного метода в другой. Для простоты рассмот-ривается пропозициональный случай.

Глава 2. Здесь рассматриваются вопросы использования локальных методов в качестве аппарата для доказательства разре-

- 15 -

шиыости некоторых классов формул и для построения эффективных разрешающих алгоритмов.

При поиске вывода методом резолюций пространство поиска растет в трех направлениях: во-первых, возрастает количество выведенных дизъюнктов, во-вторых, растет длина самих дизъюнктов, т.е. количество литер в них; в-третьих, растет сложность аргументов литер, т.е. глубина суперпозиции термов.

При реализации метода резолюций на ЭВМ требуется специальная организация памяти для хранения дизъюнктов и литер переменной длины. Сложная организация хранения дизъюнктов сильно влияет на эффективность алгоритма поиска. Различные стратегии поиска позволяют частично ограничивать те или иные параметры пространства поиска. Например, стратегия с множеством поддержки и стратегия поглощения позволяют ограничить количество выводимых дизъюнктов, не ограничивая, вообще говоря, их сложности. Стратегия предпочтения одночленов дает ограничения на длину дизъюнктов. Стратегия упорядочения литер в некоторых случаях дает ограничения на сложность тернов.

С целью ограничения сложности пространства поиска часто используются какие-либо специальные формы представления дизъюнктов. Например, если исходные дизъюнкты имеют длину, не превосходящую 2 (кромовские дизъюнкты), то в результате при- . менения правила резолюции порождаются не более чем двучленные дизъюнкты. Приведение формулы к предваренной нормальной форме со скулемовским префиксом (т.е. префиксом вида УЗ") позволяет организовать поиск вывода таким образом, что в выводимых дизъюнктах нет суперпозиций функциональных символов. Если в псоцессе поиска вывода удается ограничить как длину дизъюнктов, так и сложность термов, входящих в них, то из данного

множества дизъюнктов можно вывести не более чем конечное мно-

- 16 -

жество дизъюнктов. Это обстоятельство позволяет использовать метод резолюций в качестве основы разрешающего алгоритма для многих разрешимых классов .

Ограничения на длину выводимых дизъюнктов могут быть следствиями ограничений на вид формулы.

В качестве примера таких ограничений можно привести определение известного разрешимого класса: он содержит формулы, в к.н.ф. которых положительные дизъюнкты одночленны, все остальные дизъюнкты отрицательны. Легко видеть, что при любом применении правила вывода одна из посылок положительна и одночленна, а длина резольвенты строго меньше длины другой (отрицательной) посылки. Множество таких выводов конечно, откуда и следует разрешимость этого класса формул.

Другой пример класса формул, для которого можно ограничить длины дизъюнктов, класс формул с кромовской матрицей, т.е. предваренных формул в к.н.ф. которых дизъюнкты не более чем двучленны. При любом применении правила резолюции с двучленными посылками резольвента также не более чем двучленна. Зднако длина вывода при этом может быть и неограниченной.

Более тонкие ограничения на вид формулы , которые позво-пяют ограничить длину дизъюнктов, могут быть сделаны в терми-*ах ограничений на списки аргументов литер. Некоторые ограничения такого вида, полученные автором, приведены в работе.

Две литеры назовем экстенсиональными над множеством термов Т, если множества их аргументов совпадают с Т.

Дизъюнкт (или множество дизъюнктов) назовем однородным 1ад множеством термов Т, если любые две литеры, входящие в 1его, экстенсиональны над Т.

Нетрудно показать, что класс к.н.ф. формул_ в которых зсе дизъюнкты однородны, разрешим по выполнимости.

- 17 -

Метод резолюций является разрешающим алгоритмом для описанного класса формул.

Приведем другой пример ограничений на вид формул, которые позволяют ограничивать длину дизъюнктов.

Будем говорить, что дизъюнкт обладает свойством префикса (или дизъюнкт является префиксным), если для любых двух его литер список аргументов одной из них является началом списка аргументов другой.

Используя стратегию упорядочения литер метода резолюций, можно доказать, что класс формул, дизъюнкты которых префикс-ны, разрешим по выполнимости.

Накладывая ограничения на вид формул, можно получить выводы, в которых ограничивается сложность термов.

В качестве меры сложности термов можно использовать, например, понятие ранга терма (т.е. глубины суперпозиции функциональных символов).

При некоторых ограничениях на вид исходных дизъюнктов можно доказать, что ранги тернов в выводимых дизъюнктах ограничены.

Рассмотрим класс предваренных формул с префиксом вида У321 ... УХ.ЗЙ! ... ЗУ* (скуленовский префикс) и с матрицей, представленной в к.н.ф. Как известно, это класс сведения по выполнимости в исчислении предикатов.

Используя некоторое упорядочение литер, можно показать, что в выводах, построенных по стратегии с этим упорядочением, ранги тернов в дизъюнктах не превышают I. Отсюда следует, что для предваренных формул со скулемовским префиксом и кроновс-кой матрицей метод резолюций является разрешающим алгоритмом, т.к. пространство поиска ограничено двучленными дизъюнктами, в которых ранги термов не превышают I. Множество таких выводов" конечно. - 18 -

Аппарат таких ограничений можно распространить на более сложные случаи разрешимых классов. Можно сформулировать стратегию поиска, которая является разрешающим алгоритмом для класса К , предложенного С.Масловын и обобщающего многие известные разрешимые классы формул логики предикатов.

Обычно определения разрешимых классов логики предикатов формулируются в терминах ограничений на вид префикса формулы, на вид матрицы предваренной формулы . Понятие Г-'префикса, введенное С.Масловын, позволило ему дать более гибкое определение некоторого разрешимого класса,'названного им классом К.

Формула Г принадлежит классу К, если можно указать такие переменные Хь ...., Хк (К>0), не находящиеся в области действия никакого квантора существования, что каждый непустой Г-префикс удовлетворяет одному из трех условий:

1) оканчивается квантором существования,

2) имеет вид \/Я1 УХК,

3) состоит из одного квантора общности.

Элиминируя кванторы, получим бескванторную формулу, в

которой вместо 3-переменных стоят скулемовские терны. Класс формул, полученных из формул класса К элиминацией кванторов, будем обозначать через КБ.

Приведем ряд определений, которые дадут возможность описать синтаксические свойства формул класса КБ.

Терн X управляет терном 6 если выполняется хотя бы одно из условий:

1) Х=6,

2) 1, ..., "!;„), ГЪО, 6- переменная и 6=1; 1 для некоторого I, 1<1<П,

3) 1:4(1; ......1;„), б^си, ..., 1;т), п>т>о

- 19 -

Териы "Ь1 и "Ь2 называются подобными, если любой из них управляет другим.

Множество термов Т1 управляет множеством термов Тг. если для каждого терна 1гбТ2 существует терм "^Е Т1, такой, что 11 управляет

Литера А управляет литерой В, если множество аргументов литеры А управляет множеством аргументов литеры В.

Подобие множеств тернов и подобие литер определяется аналогично тому, как это было сделано для тернов.

Терн 1 называется регулярный, если он управляет каждый своим аргументом. В частности, переменные и константы регулярны тривиальным образон.. Очевидно также, что все термы ранга I регулярны.

Множество тернов называется регулярный, если оно либо не содержит термов положительного ранга, либо в него входит регулярный терн положительного ранга, управляющий всеми термами этого множества (этот терн называется управляющим термом множества).

Литера называется регулярной, если множество ее аргументов регулярно.

Множество М литер называется К-регулярнын, если выполняются следующие условия:

1) М состоит из регулярных литер,

2) К не превосходит минимальной из размерностей функциональных символов, входящих в И,

3) в И входит литера, управляющая всеми литерами из Н,

4) неунарные литеры нулевого ранга подобны друг другу и множество их аргументов подобно множеству первых К аргументов любого терма положительного ранга, входящего в литеры из М.

Дизъюнкт называется регулярным, если множество его литер

- 20 -

К-регулярно для некоторого К.

Множество литер Mi называется компонентой множества литер М, если MicM и ни одна переменная, входящая в литеры из Mi, не входит в литеры из M-Mi. М называется неразложимым множеством, если у него нет компонент, отличных от пустой и от М, в противном случае М называется разложимым. Множество литер называется квазирегулярныи, если все его неразложимые компоненты регулярны. Аналогично определим регулярные и квазирегулярные дизъюнкты.

В работе показано, что для всякой противоречивой формулы F из KS существует вывод пустого дизъюнкта в резолюционном исчислении , в котором все выводимые дизъюнкты квазирегуляр-ны. Доказав далее, что количество таких выводов ограничено, мы получим доказательство разрешимости класса К.

Глава 3. В этой главе описан вариант метода резолюций

для нескулемизированных формул.

Применение метода резолюций требует преобразования формулы в множество дизъюнктов, и каждый дизъюнкт - это дизъюнкция атомарных формул и их отрицаний. Для приведения формулы к такому виду используется эквивалентное преобразование, называемое скулемизацией, т.е. элиминация кванторов путем введения скулемовских термов вместо 3-переменных.

Однако скулемизация в некоторых случаях бывает невозможна или нежелательна: она расширяет язык, увеличивая пространство поиска, усложняет алгоритм унификации, интерпретация скулемовских термов может оказаться неконструктивной, что может повлиять, например, на возможность извлечения программы из доказательства.

Для того, чтобы избежать скулемизации и обойти труднос-

- 21 -

ти, возникающие при упрощении формул вида ЭХ(В(Х) &С(Х)), воспользуемся дедуктивно эквивалентным преобразованием формулы в множество дизъюнктов путем введения новых предикатных переменных.

При таком преобразовании формула Г преобразуется в конъ юнкцию формул, каждая из которых имеет вид УФ) или V ЗхР, где й - дизъюнкция литер, Р - литера. Эти формулы мы по-прежнему будем называть дизъюнктами формулы Г.

Сформулируем исчисление для поиска опровержения множества дизъюнктов описанного вида, соответствующих некоторой формуле Г.

Аксиомами исчисления являются дизъюнкты формулы Г (исходные дизъюнкты). Выводимые объекты этого исчисления -дизъюнкты вида У(Р).

Правило рывода Ва.

У(АУ С) У(ВУ Р) У(СУ 0)б

где А, В, С, 0 - дизъюнкции литер, б - У-унификатор множества атомов, входящих в А и в В.

Правило вывода Вв.

У(АУ С) У ЗдР(х) У (С б)

где б=б 16 2. <5 1 - У-унификатор для множества атомов из А, б 2 - 3-унификатор для атомов Аб ± и Р(Х), переменная X не входит в (Сб ).

Алгоритм унификации для этих правил существенно проще алгоритма для обычного метода резолюций.

Имеет место теорема о непротиворечивости и полноте описанного исчисления.

Глава В этой главе описан вариант метода резолюций

- 22 -

идя модальных логик.

Язык математической логики широко используется в настоя-цее время как язык программирования, как средство представления знаний в экспертных системах и других интеллектуальных :истемах. Достаточно упомянуть в этой связи PROLOG и его многочисленные расширения, в том числе и расширения средствами модальной логики . В последнее время значительный интерес вызывают неклассические логики (модальные, временные и др.) как наиболее адекватное средство представления знаний в различных зредметных областях. При реализации на ЭВМ предпочтение отда-этся локальным логическим системам, в частности, системам ре-юлюционного типа.

В этой главе описан вариант метода резолюций, основанный ia семантике, являющейся некоторой конкретизацией стандартной :емантики Крипке и не выходящей за пределы логики первого порядка. Использование лишь средств логики первого порядка поз-тляет без труда перенести все известные результаты о полноте :тратегий поиска для классического исчисления предикатов на юдальные исчисления. Предлагается некоторая стратегия поиска (ывода, которая является разрешающим алгоритмом для пропози-;иональной логики S4. Описанный метод годится не только для >4, но без труда распространяется и на другие модальные сис-•емы (S5, т, К« и др.). Различие будет лишь в алгоритмах уни-)икации,а формулировки правил вывода остаются без изменений, 'акже не представляет затруднений распространение метода на [счисление предикатов.

Опишем теперь погружение логики S4 в исчисление предика-ов, отличное от простого перевода семантики Крипке.

Каждой формуле А логики S4 и произвольной переменной О оставим в соответствие некоторую формулу логики предикатов

- 23 -

Рг(А, Ю) с функциональный Сймволок который будет далее обозначать асоциативную операцию конкатенации слов.

Каждой атомарной формуле р поставим в соответствие одноместный предикатный символ Р и определим формулу Рг(А, Ш) следующим образом:

- Рг(р, и) = Р(«), где Р - атом, Р - соответствующий ему предикатный символ.

Ниже В и С обозначают произвольные модальные формулы.

- Рг(В &£. м) = Рг(В, и) бРг(С, м).

- Рг(ВУ С, и) = Рг(В, ю)У Рг(С, и).

- Рг(В=> С, и)) = Рг(В, м)=> Рг(С, и).

- Рг< 1 В. и) = 1Рг<В, м).

- Рг([]В. и) = Ух(Р2(В, И*Х)), где I - новая переменная, не входящая в Рг<В, И).

- Р2<< >В, Ш) ¡= Э1<Рг(В, 61*1)), где X - новая переменна«

Предикатных переводом модальной формулы А назовем формулу Рг(А, ПИ). Очевидно, что перевод пропозициональной формулы А - замкнутая предикатная формула.

Таким образом, мы свели задачу поиска вывода модальной формулы из задаче поиска вывода предикатной формулы. Дл$ приска вывода предикатной формулы будем использовать метод резолюций.

Для облегчения изложения мы будем считать, что модальна: формула ТА уже преобразована к множеству дизъюнктов методом введения новых переменных : каждой неэлементарной подформуле В. исходной формулы А ставим в соответствие пропозициональную переыенную ё и формулу А преобразуем к виду [](ё О В) &А', где А' подучена из А заменой В на ё. В результате такого пре образования А преобразуется в множество дизъюнктов, имеющих один из видов [](РУ ОУ 1Ъ, []<РУ ПО), [](РУ <>0), Р, гд

- 24 -

Р, О, И - литеры. Для каждого из этих дизъюнктов построим его предикатный перевод, элиминируем кванторы введением скулемов-ских функций, в результате получим множество дизъюнктов Эа. Добавим к этому множеству множество дизъюнктов ,'соответствующих аксиомам равенства и аксиомам, описывающим свойства конкатенации.

Известны модификации метода резолюций, учитывающие спе- • цифику теории, в которой он применяется. В частности, усложнив алгоритм унификации, можно удалить из множества первоначальных дизъюнктов дизъюнкты , описывающие свойства операции конкатенации. Полученную в результате систему будем называть резолюцией с ассоциативной унификацией. Алгоритм ассоциативной унификации может быть получен модификацией стандартного алгоритма унификации.

Алгоритм ассоциативной унификации может породить множество независимых унификаторов, но для случая, когда составляющие унифицируемых термов различны, это множество конечно.

Можно показать, что при записи тернов нет необходимости в сохранении аргументов скулеиовских функций, и эти функции можно заменить константами. В результате такой замены мы получим новое представление модальных формул и правило резолюции для них:

А(и) V В 1 А(Ц) V С (ВУ С)б

где 11 и О -ассоциативные термы с константами вместо функциональных символов, б - н.о.у. для тернов и и О.

Доказана теорема о непротиворечивости и полноте описанного метода поиска вывода.

Поскольку описанное исчисление резолюций получается погружением & в классическую предикатную революционную систему»

- 25 -

то для модальной резолюции оказываются полными все полные стратегии, известные для предикатного исчисления резолюций.

Описанный метод резолюций с ассоциативной унификацией характеризуется быстрым ростом пространства поиска, т.к. алгоритм унификации выдает не единственный унификатор. Предлагается стратегия поиска, которая ограничивает пространство поиска и может служить основой разрешающего алгоритма для пропозициональной логики S4.

Глава 5. В этой главе описаны реализации локальных методов, и стратегий, предложенных автором.

Предложенная автором стратегия поиска, на основе которо! доказана разрешимость класса К,была реализована в ИК АН ЭССР г.Таллинн. О результатах реализации было сообщено в публикациях, где отмечалась высокая эффективность стратегии не толь ко для формул класса К но и для произвольных формул исчисления предикатов. Программа разрешила все формулы из монографи: А.. Черча, как общезначимые, так и необщезначимые. Наибольшее время поиска вывода для этих формул составило менее 3 минут на ЭВМ типа IBM PC/AT. Программа разрешила также многие тестовые проблемы, известные в литературе по автоматическому до касательству теорем (например, проблема, известная под назва нием "паровой каток", была разрешена менее,чем за 4 минуты). Были разрешены другие тестовые примеры, долученные, например погружением в исчисление предикатов модальных и интуиционист ской логик .

Большая Часть главы посвящена описанию одной реализации локальных методов поиска вывода, которая была выполнена в Ка занском Государственном Университете под научным руководство автора диссертации.

Система СИНТЕЗ, разработанная в КГУ, предназначена да автоматического решения так называемых технологических »адач.

Центральная идея, положенная в основу реализации системы :ИНТЁЗ, - это идея декомпозиции решаемой задачи на подзадачи, соторые в свою очередь тоже могут быть сведены к подзадачам, 'акая декомпозиция должна быть доведена пользователем до гровня элементарных действий, которые реализуются модулями, шешними по отношению к системе. Правила декомпозиции каждого [еэлементарного действия должны быть описаны пользователем, и ювокупность этих правил образует технологическую модель [редметной области (ТМО).

Решением задачи является последовательность элементарных ;ействий, которая синтезируется системой на основе правил, вписанных в ТМО.

При описании декомпозиции действий пользователь может :спользовать несколько типов декомпозиции: сложное действие ожет синтезироваться из поддействий путем конкатенации, ростого и табличного объединений, рассмотрения вариантов, ыбора. При объединении действий учитывается дополнительная нформация, описывающая некоторые требования на порядок вы-олнения действий (контексты).

Глобальный учет этих требований и проверка их совместности реализованы на идеях логического программирования. Для того по технологической модели предметной области составля-тся логическое исчисление, формулы которого выражают следую-ий смысл: "если выполнимы все поддействия действия О и удов-етворены все условия , накладываемые контекстами, то выпол-имо и действие СГ.

Конкретный вид аксиом зависит от способа декомпозиции

- 27 -

действия на поддействия и от вида контекстных условий. Затеи построенном исчислении доказывается высказывание о выполнимости целевого действия. Поиск доказательства производится автоматически. Конкретный вид аксиом позволяет организовать поиск с линейной сложностью. Наконец, по найденному доказательству строится требуемая последовательность действий: из последовательностей действий, реализующих поддействия, синтезируется последовательность действий, реализующая само дейст вие. Способ соединения последовательностей в результирующую последовательность зависит от способа декомпозиции этого дей ствия.

Таким образом, метод автоматического решения задач в системе СИНТЕЗ состоит из следующих шагов :

1) Построение логического исчисления по ТМО .

2) Поиск доказательства целевого высказывания .

3) Извлечение решения из доказательства (синтез).

Такой метод, использующий дедуктивную модель задачи

(т.е. логическое исчисление), является характерным для логического программирования и лег в основу хорошо известных сис тем логического программирования PROLOG, ПРИЗ и др. Эти системы отличаются друг от друга типами логического исчисления, алгоритмами поиска доказательства и способами извлечения ответа из доказательства.

Охарактеризуем сферу применимости системы, тип задач, для которых система является удобным средством.

Для многих прикладных областей характерна следующая схе ма деятельности. Специалист-конструктор создает замысел изде лия, специалист-технолог разрабатывает технологию изготовления изделия, а исполнитель реализует этот процесс на некотором оборудовании и получает требуемое изделие.

- 28 -

При этом под изделием может пониматься как какая-либо :онкретная продукция (деталь, химический препарат, программой продукт и т.п.), так и , допустим , новые знания , приоб-»етенные обучаемым в процессе автоматизированного обучения.

Под оборудованием также может пониматься широкий набор :редств - от сложных механизмов и устройств (станки, ЭВМ, хи-гаческие приборы и т.п.) до ничем не вооруженных человеческих >ук.

В приведенной схеме наибольшие успехи достигнуты на пос-1еднем этапе - достаточно вспомнить управляемые роботы, стан-:и с программным управлением и т.п.). Первый этап этой схемы конструирование - является наиболее творческим и менее дру-■их этапов поддается автоматизации. Что касается, второго эта-;а - разработки технологического процесса - то это по-видймо-|у - наиболее реальная область применения машинно-ориентиро-1анных методов автоматизации интеллектуальной деятельности.

Оказалось возможным применить дедуктивный подход к реше-[ию задач разработки технологических процессов (эти задачи в ;альнейшем мы будем называть технологическими задачами).Воз-южность автоматизации решения технологических задач базируйся на характерных особенностях предметных областей, в кото-1ых возникают такие задачи. Первой особенностью является на-;ичие знаний, позволяющих сводить задачи к подзадачам. Второй 'собенностью является статичность пространства поиска, т.е. то неизменяемость в процессе поиска (под пространством поис-:а здесь понимается множество индивидов и отношений между ни-[и). Размеры пространства поиска могут быть оценены до начала оиска решения и зависят от некоторых характеристик предмет-;ой области и конкретной решаемой задачи.

Поиск решений технологических задач основан на идеях ло-

- 29 -

гического программирования. При решении задач используются технологические знания, которые описывают предметную область и конкретные факты, описывающие конкретную задачу. Технологи ческие знания записываются в виде некоторой формальной систе мы, а конкретные факты.задаются в виде таблиц. Язык формальной системы - логика предикатов первого порядка с ограниченными кванторами.

По ТМО и таблицам строится вспомогательное пропозициональное исчисление, аксиомы которого - хорновские дизъюнкты, а единственным правилом вывода является Ш0С1иб РОПЕПЛ. В этом исчислении доказывается утверждение о существовании решения целевой технологической задачи. По полученнму доказательству строится последовательность элементарных действий, реализующих требуемый технологический процесс. Эта последовательност и является решением целевой задачи.

Описанный подход был реализован на некоторых предметных областях.

Технологическая модель механической обработки описывает правила проектирования технологического маршрута для плоских деталей." Эти правила позволяют выбрать правильную последовательность обработки поверхностей в зависимости от их взаимно го расположения, выбора базовых поверхностей, от размеров, требований на чистоту и точность обработки, а также спроектировать последовательность обработки сложных поверхностей. Технологическая модель была разработана по хозяйственному договору между Казанским университетом и предприятием К Ф НИАТ в рамках темы № 948 "Исследование, разработка и внедрение робототехнических комплексов (РТК) и гибких производственных систем (ГПС) для механической обработ:.;- деталей на обслуживаемых предприятиях", включенной в отраслевой план работ по

- 30 -

:озданию гибких производственных систем. Результаты работы шли переданы в опытную эксплуатацию на предприятия г. Казани 1 г. Ленинграда и используются для решения задач проектирована технологических процессов.

В качестве другого примера можно привести технологичес-<ую модель формирования чертежа. Технологические правила опирают правила описания чертежей на языке ЯКОБ .Они отражают 1екоторые требования ГОСТ на оформление чертежей для класса деталей типа тел вращения. Технологическая модель разработана ю договору № 183/88 о научно-техническом содружестве с од-шм из предприятий г.Ленинграда и передана для использования.

Заключение.

В области автоматизации поиска вывода , в теории и практике использования методов резолюционного типа автором получен ряд новых результатов,которые легли в основу диссертации:

О) получен и обоснован общий метод доказательства полноты стратегий в методе резолюций и обратном методе, метод получения двойственных стратегий;

6) получен метод резолюционного типа для нескулемизиро-ванного варианта исчисления предикатов, при этом даны : новое эпределение дизъюнктов,более простой,чем традиционный, алгоритм унификации, более.простые правила вывода,являющиеся частными случаями традиционного правила, даны доказательства корректности и полноты метода;

Оразработан метод резолюций для модальных логик, обоснован метод доказательства полноты стратегий для них,доказана полнота некоторых стратегий;

сЬполучены разрешающие алгоритмы на базе метода резолю-- 31 -

ций для ряда разрешимых классов: класс К, класс формул с пре фиксом V*3* и кромовской матрицей,модальные логики S4, S5, всех разрешающих алгоритмах использована общая идея поиска вывода .удовлетворяющего стратегии с упорядочением (разные упорядочения для разных классов);

В) разработан логический аппарат системы СИНТЕЗ для автоматизированного решения технологических задач; система pea лизована коллективом сотрудников кафедры прикладной математи ки КГУ под научным руководством автора диссертации.

Список работ, опубликованных по теме диссертации.

1. Замов Н.К., Шаронов.В.И. Разрешающие тактики поиска в методе резолюций. //Тезисы докл. III Всесоюзн. конф. по матем. логике.-Новосибирск, 1974.- С. 75 - 77.

2. Замов Н.К., Михайлов В.Ю. Вопросы сложности дедуктивных средств решения технологических задач. //Семиотические аспекты формализации интеллектуальной деятельности . Тезисы докл. и сообщ. Школа-семинар "Кутаиси - 85".- М.,1985.-С.209 - 212.

3. Замов Н.К., Михайлов В.Ю. Логические средства автоматического решения технологических задач. //Тезисы докл. Всесоюзн. конф. по прикладн. логике.- Новосибирск, 1985.-С.79 - 81.

4. Замов Н.К. Метод резолюций без скулемизации.//Докл. АН СССР,- 1987.- Т. 293,- te 5,- С. 1046 - 1049.

5. Замов Н.К. Метод резолюций без скулемизации и разрешимые классы. //Семиотические аспекты формализации интеллектуальной деятельности. Тезисы докл. и сообщ. Школа-семина

- 32 -

Воржоыи - 88",- М.,1988.- С. 103 - 105.

6. Занов Н.К. Модальные резолюции. //Известия вузов, атенатика,- Казань, 1989.- № 9.- С. 22-29.

?1Ьос1 шс1 Шв 1пивгав МвИчос!. /А&сХ. Мед 1п Coшpat. 1987.- \1.278.- Р. 501 - 505. 8. Еашои М. Ма&Еои'л Гпивгав МеШос! апс1 0вс1<М£в [!а^вд.//Мпа<Ед о| Ригв шс1 Арр-М Ьозьс.- №юШ-НоШи1. )89.- V. 42.- N0 2,- Р. 165 -194.

7. 2отои N. К. Оп а Соппвсйоп Ввййввп ТНв ВвлоМьоп