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

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

Ларионов Дмитрий Сергеевич

ОБРАТНЫЙ МЕТОД УСТАНОВЛЕНИЯ ВЫВОДИМОСТИ ДЛЯ АВТОЭПИСТЕМИЧЕСКОЙ ЛОГИКИ И ЕГО ПРИМЕНЕНИЕ В ЭКСПЕРТНЫХ СИСТЕМАХ

05.13.01 — Системный анализ, управление и обработка информации (отрасль: информация и информационные системы)

Автореферат диссертации на соискание ученой степени кандидата технических наук

Томск - 2005

Работа выполнена в Томском политехническом университете

Научный руководитель:

доктор технических наук, профессор В.К. Погребной

Официальные оппоненты:

доктор технических наук, профессор В.А. Силич

кандидат физико-математических наук, доцент В.В. Бурлуцкий

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

Защита состоится 21 декабря 2005г. в 15 ч. на заседании диссертационного совета Д212.269.06 при Томском политехническом университете по адресу: 634034, г.Томск, ул.Советская, 84, институт «Кибернетический центр» ТПУ, ауд.214.

С диссертацией можно ознакомиться в библиотеке Томского политехнического университета по адресу: 634034, г. Томск, ул. Белинского, 53.

Автореферат разослан «/У» ноября 2005г.

Ученый секретарь диссертационного совета

Институт математики СО РАН, г. Новосибирск

к.т.н., доцент

М.А. Сонькин

*-------' 3

Общая характеристика работы

Актуальность работы. В последнее время интенсивно рассматриваются вопросы автоматизации процессов получения решений компьютерными программами - это связано не только с классическими задачами искусственного интеллекта доказательства теорем и построения советующих экспертных систем, но и с бурным развитием и внедрением в производственный процесс корпоративных информационных ERP-систем, CRM-систем, программ управления технологическими процессами, задач извлечения данных и знаний' анализ данных, анализ документов, поиск по смыслу в Internet, распознавание текста и т. д. Несмотря на то, что для решения указанных вопросов успешно применяются такие технологии, как нейронные сети, семантические сети и фреймы, набирает рост и интерес к традиционному логическому методу хода рассуждений за счет привлечения неклассических модальных логик. Наличие большого числа эвристик в рассуждениях соответствующих систем, их неспособность всегда четко обосновать свое решение ставят под сомнение применение нелогических способов рассуждений. В свою очередь, вывод, опирающийся на одну из модальных логик, сохраняет строгость и обоснованность классических аксиоматических систем вывода, однако при этом он гибок за счет наличия операторов □ (необходимости) и 0 (возможности). Так же многие модальные логики обладают свойством немонотонности, позволяющим пересматривать свои выводы в процессе рассуждения. В частности, проблему построения доказательства заданного целевого утверждения для экспертной системы можно свести к проблеме поиска вывода формул определенного логико-математического языка в соответствующем исчислении. Имеются многочисленные работы, как в области теории логического вывода в классическом исчислении предикатов и теории разрешимых фрагментов этого исчисления, так и в области практического построения алгоритмов программ автоматического поиска вывода. Однако для успешной практической формализации желательно, чтобы методика построения алгоритмов автоматического поиска вывода допускала расширение на различные неклассические системы. Большой интерес представляют разнообразные модальные системы, которые позволя1^_шщдьтатъ_такие понятия

рос - '1-А«:1»ная В' ; rFKA

РК

предметной области, как «необходимо», «возможно», «известно» и ряд других. Большинство предлагаемых алгоритмов поиска вывода основано на теореме Эрбрана, формулирующей необходимые и достаточные условия выводимости формулы Однако практическая реализация с помощью данной теоремы приводит к порождению большого числа излишних дизъюнктивных членов. Существует множество методов, сокращающих поиск доказательства. Одновременно с методом резолюций Д.А. Робинсона и независимо от него С.Ю. Масловым был предложен «обратный метод» поиска вывода. Он дает возможность целенаправленно, опираясь на конкретные особенности доказуемой формулы, ограничить перебор, возникающий при непосредственном применении теоремы Эрбрана и получить вывод более экономным способом. На данный момент существует целый ряд реализаций программ автоматического поиска доказательств на основе неклассических логик, основанных, как правило, на методе резолюций или его модификациях. В то же время, наиболее эффективная программа автоматического поиска доказательства, основанная на обратном методе - система /("-обратное К -была реализована в 1999г. А.Воронковым. Помимо этого существует целый ряд работ Т.Таммета и Г.Минца, посвященных реализации обратного метода для таких неклассических логик, как Б4, линейной и интуиционистской логик. В работе В.В.Бурлуцкого 2001 года рассмотрено применение системы КТ (или «логики знания») в качестве основы для обратного метода установления выводимости.

Следует отметить, что до сих пор в указанном выше контексте подробно не была рассмотрена такая важная неклассическая система, как Б5 или автоэпистемическая логика. Эта логика обладает важным свойством немонотонности, в ее рамках рассуждения интроспективны и идеально-разумны. В ней модальный оператор □ принимает значение «предполагается», а оператор 0 - «обратное не предполагается». Такая трактовка оператора необходимости позволяет нам говорить о широком спектре применимости экспертных систем, логической моделью машины вывода которых является логика 55 и позволяет рассчитывать в дальнейшем на возможность перехода к оперированию «персонифицированными» знаниями.

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

Цель работы и задачи диссертации. Проблема построения механизма вывода для экспертных систем (ЭС), прежде всего, связана с наличием неопределенности в фактах, используемых системой. В работе Ларионова Д.С. и Новосельцева В.Б. (2002г.) рассмотрена оболочка ЭС с прямым и обратным выводом, использующая коэффициенты определенности (КО) относительно фактов, с которыми она работает; имеется также ее реализация на языке логического программирования Visual Prolog. Несмотря на то, что КО вычисляются, отчасти, на основе теории условной вероятности, рассуждения и вывод оболочки имеют эвристическую составляющую, которая не всегда четко обозначена, и не каждый раз получена достоверным способом. Применение КО можно заменить математически обоснованным выводом с применением модальной логики, хотя в ее контексте в противовес классической логике понятие общезначимости зачастую заменяется понятием выполнимости, так как автоэпистемическая логика формализует эволюционирующие рассуждения немонотонного типа.

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

Для реализации поставленной цели следует решить следующий комплекс задач:

• Исследование синтаксиса и семантики автоэпистемической логики, а также ее свойств: полноты, легальности, устойчивости и т.д.

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

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

• Выявление и описание стратегий сокращения пространства поиска вывода, таких как:

> избавление от избыточных секвенций;

> введение понятия упорядочения вывода, в зависимости от структуры доказуемой формулы;

> использование понятия предпосылки для удаления предпосылающих секвенций.

• Формулировка общего алгоритма установления выводимости.

• Практическая реализация указанного выше алгоритма и демонстрация его использования.

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

Научную новизну полученных в работе результатов определяют:

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

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

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

4. Применение и адаптация алгоритмов стратегий сокращения пространства поиска вывода логик К и КТ для автоэпистемической логики КТ45 (S5).

Практическая ценность заключается в следующем:

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

2. Способность совместного применения методов движения по дереву вывода, таких как «сверху-вниз» и «снизу-вверх», что дает возможность использовать частные свойства конкретного доказываемого или проверяемого факта экспертной системы.

3. Построение программного модуля «Система проверки утверждений на основе модального вывода», реализующего алгоритм обратного метода установления выводимости. Модуль реализован в визуальной среде разработки Delphi 7.0 на объектно-ориентированном языке Object Pascal и функционирует под управлением операционной системы Windows 2000.

4. Примером реализации вышеуказанного модуля является его использование в Отделении ПФР по Томской области для оценивания гипотез актуарных расчетов, а также на заводе ОАО «Маногомь» для логического анализа производственной мощности предприятия. Внедрение подтверждено соответствующими документами.

Основные положения, выносимые на защиту

1. Реализация алгоритма обратного метода установления выводимости для автоэпистемической логики.

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

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

4. Различные стратегий сокращения пространства поиска вывода. Алгоритм Ф-упорядочения. Теоремы полноты для исчислений с учетом всех стратегий с доказательством.

5. Практическое применение алгоритма обратного метода установления выводимости и вывода на основе автоэпистемической логики: «Система проверки утверждений на основе модального вывода». Области ее применения, подтвержденные соответствующими заключениями.

Апробация работы. Основные результаты работы докладывались и обсуждались на следующих конференциях:

• Девятый Российско-Корейский международный симпозиум по науке и технологиям (The Eights Korea-Russian International Symposium on Science and Technology) «KORUS 2005» (г. Новосибирск, НГТУ, 26 июня - 2 июля 2005 г.).

• Одиннадцатая международная конференция по вычислительной механике и современным прикладным программным системам (Москва-Истра, РОССИЯ, Московский авиационный институт (Технический университет) 2-7 июля 2001 г.).

• XXIII Конференция молодых ученых механико-математического факультета МГУ им М.В.Ломоносова (г. Москва, МГУ, 9-14 апреля 2001 г.).

• XXII Конференция молодых ученых механико-математического факультета МГУ им М.В.Ломоносова (г. Москва, МГУ, 17-22 апреля 2000г.).

• XXXVIII Конференция «Научно-технический прогресс» (г. Новосибирск, НГУ, 2-5 апреля 2000г.).

• IV межвузовская конференция аспирантов и молодых ученых «Наука и образование» (г. Томск, ТГПУ, 24-29 апреля 2000г.).

/

• Ш межвузовская конференция «Математика: ее содержание, методы и значение» (г. Томск, ТГУ, 23-29 апреля 2001г.).

По результатам работы имеется 10 публикаций, в том числе 2 статьи в реферируемых отечественных изданиях (МатематичеЬкое Моделирование и Известия Томского Политехнического Университета). Личный вклад.

1. Автором предложено использование в качестве механизма вывода автоэгшстемической логики. Ранее в различных работах был рассмотрен подход, основанный на менее выразительных логиках К и КТ (логика знания). В связи с этим исследованы свойства системы S5 и выделены ее отличительные черты, например, немонотонность.

2. На систему S5 автором успешно спроецированы базовые и обратные системы исчислений секвенций, исчислений путей, ранее известные своим применением на логиках К и КТ. Построены соответствующие системы исчислений , SS9^, SfPah и £5V

3. Автор исследовал свойства исчислений 55&9 , §5Ф¡т. , S50Pall, , 85Ф1Р и математически строго доказал их главное фундаментальное свойство - полноту, что дает уверенность в том, что механизм вывода экспертной системы, построенный на основе исчисления (S5">)m,), будет давать корректные результаты.

4. С целью сокращения пространства поиска вывода для системы S5 автором приспособлены различные критерии избыточности, ранее применяемые для систем К и КТ. В зависимости от применения конкретного критерия получаются различные исчисления S50 '¡Р, S5'" ''ip, {SS^'^ip}, для которых доказаны теоремы

полноты. Как промежуточный результат, автором получен алгоритм Ф-упорядочения, применение которого существенно сокращает длину вывода.

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

/ 10 6. Автором получен общий алгоритм обратного метода установления выводимости

для автоэпистемической логики.

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

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

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

В первой главе описывается модальная система £5, называемая автоэпистемической логикой. Затем вводится понятие мультимножества и исчисления секвенций. Далее строятся - прямое исчисление секвенций и 85ф1г<у - обратное исчисление секвенций на основе автоэпистемической логики.

Суть автоэпистемической логики раскрывается путем описания ее синтаксиса и семантики, указываются аксиомы, составляющие систему 55. С помощью модели Крипке (IV., /?, V) показывается семантическая полнота автоэпистемической логики и ее легальность относительно множества основных предположений. Рассматривается также ее важнейшее свойство немонотонности, позволяющее механизму вывода ЭС, основанном на аксиомах и правилах логики 55, вести эволюционирующие рассуждения.

Предлагаемая реализация обратного метода для логической системы 55 основана на исчислении путей, впервые описанном А.Воронковым в 2000г. Далее это исчисление путей было распространено на «логику знания» КТ В.В.Бурлуцким в 2001г.

Пусть Ф - данная формула логики 55. Для поиска доказательства Ф мы будем использовать не саму систему 55, а эквивалентное ей исчисление секвенций 55^,. Схематично это секвенциальное исчисление задано на рисунке 1.

Аксиомы: Г, р, ~р. Правила вывода-.

Г. А. В (л); Г.А Г.В (v); Г^А_ (0); Г.А <□).

Г,АаВ Г,А^В аГ,0А, Д Г, пА

Г. оА (4), Г, 0А (5). Г, сшА Г, оОА

Рисунок 1. Исчисление секвенций 55«^

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

Теорема полноты 85^. Формула Ф системы 55 является невыполнимой тогда и только тогда, когда она имеет опровержение в

Поиск опровержения мы переносим в «обратное» исчисление которое

зависит от целевой формулы Ф. Схематично 55">;т,, задано на рисунке 2.

Аксиомы: р, ~р. Правила вывода:

Г.А. А (С); Г.А А.В (V); Г.А (л,); Г.В (л,);

Г, А Г, Д, А^В Г,АлВ Г,АлВ

ГдА_(0); Г_ (0+); Г,А_(о);

□Г,0А аГ,0А Г, оА

Г. оА (4); Г. ОА (5).

Г, сшА Г, аОА

Рисунок 2 Исчисление секвенций 55ф

Заметим, что не любая невыполнимая секвенция имеет опровержение в

поэтому непосредственное доказательство теоремы полноты для невозможно.

Для доказательства полноты 55<р/„у мы используется лемма подсеквенциальности,

которая позволяет перенести поиск опровержения Ф в исчисление Б5ф1т..

Лемма подсеквенциальности для Пусть Ф - формула Б5 и Г - секвенция,

состоящая из подформул Ф и имеющая опровержение в 55.^, тогда существует секвенция А такая, что ДяГ и Л имеет опровержение в 55Ф/„„ Далее доказывается следующая теорема полноты.

Теорема полноты Формула Ф системы 55 является невыполнимой тогда и

только тогда, когда она имеет опровержение в 55Ф!т1.

Во второй главе рассматривается прямое исчисление путей 55<*>/.яА, поиск дерева вывода в котором технически проще и нагляднее, чем в Аналогично, для 55Ф/т. вводим обратное исчисление путей 55Ф1Р. Для этих целей вводятся определения пути и подформулы.

Исчисление путей 55<#,.0,А схематически задано на рисунке 3.

Аксиомы: Г, пищ. Правила вывода-

Г. ял}, ялг (л); Г. тгУ| Г.яуг (v); Пр.яО (0): По. яа (□): Г,я Г,я: Г, П, я П, я

Пор, пар (4); ПпО. яоО (5). Па,па Па, ка

Все пути, входящие в секвенции путей (П = я>, . ., я„, и Па ~ л ¡а, ..., л„а)

являются Ф-путями В аксиомах р = Ф lni , ~-р = Ф /„2, для некоторой

пропозициональной переменной р.

Рисунок 3. Исчисление путей S50Path

Определение. Образом формул последовательности путей или дерева вывода в S5 ра,н называется соответственно последовательность выводов или дерево вывода, полученное из первоначальных заменой каждого пути гена формулу Ф /х. Для доказательства теоремы полноты S50Palt, необходима следующая лемма (в

работе приводится с доказательством).

Лемма бимоделирования для S5®p,th

1. Пусть D - дерево вывода пустого пути в S^pah- Тогда образ D ' формул из D является деревом вывода формулы Ф в S5s,q г

2.Пусть D'- дерево вывода секвенции А¡, .... А„ в S5seq и я>, л„- такие пути, что Ф ¡к, =А,, Vî =/, п. Тогда существует дерево вывода D для я>, ..., л„в S50pa,t, такое, что D 'является образом формул дерева вывода D.

3.Пункты 1 и 2 справедливы, если везде "дерево вывода" заменить на "опровержение ".

Далее доказывается теорема полноты для SS0^-

Теорема полноты для 85фр,ш. Формула Ф логики S5 невыполнима тогда и только тогда, когда пустой путь s имеет опровержение в S50pMh.

Обратный вариант исчисления путей, полученный из S50im, указан на рисунке 4.

Аксиомы: Пи %2- Правила вывода:

Г. ЯЛ[ (Л|); Г. ял, (л,); Г. жу, A, nvr (v); Г. я. я (С)

Г,я Г,я Г, А, я Г, я

Го (0+); Пр. яО (0); Па яа (а);

Г,я П, я П, я

Про, кап (4); ПаО. яаО (5).

Па, яа Па, яп

Рисунок 4. Обратное исчисление путей S50/r

Для 55ф//> , так же как и для S50pa,h, справедливы лемма бимоделирования и

теорема полноты:

Лемма бимоделирования для 85ф|р

1. Пусть D - дерево вывода в S50ip Тогда образ D' формул D является деревом• вывода формулы Ф в S50i„x.

2. Пусть D'- дерево вывода секвенции А¡, .., А„ в 35Ф1т. и ль ..., я„ - такие пути, что Ф !л, =А, , Vi ~1,п Тогда существует дерево вывода D для /Г/, ..., п„ в S5*m такое, что D 'является образом формул дерева вывода D.

» 3 Пункты 1 и 2 справедливы, если везде "дерево вывода" заменить на

"опровержение".

Теорема полноты 85Ф|Р. Формула Ф из системы S5 невыполнима тогда и только «t тогда, когда пустой путь е имеет опровержение в исчислении SS0/?

В третьей главе исследуются свойства исчисления S50Faih и свойства деревьев

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

секвенций в пространстве поиска вывода, тем самым, сократив его.

Определение. Модальная длина пути - число вхождений модальных операторов 0 и □ в путь.

Также в работе вводятся понятия префикса пути и собственного префикса пути.

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

исчислениях S50pa,h, S50/„v вводятся определения ромборазделенных путей и путей,

образующих v-вилку. Также определяется противоречивая пара путей.

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

Лемма о ромборазделенных путях. Пусть П - последовательность путей, входящая в дерево вывода е в S50pali,. Тогда в П не существует ромборазделенной пары путей щ, щ.

Определение. Обозначим через S50' '¡Р исчисление, полученное из Sf/p:

• удалением всех секвенций путей, содержащих пути различной модальной длины;

• удалением всех секвенций путей, содержащих противоречивую пару путей. Во введенном исчислении Sf^'/p справедлива следующая лемма.

Лемма подсеквенциальности для S50'*ip. Пусть D - опровержение е в , I -вывод в D в виде:

й^Лл, Г

и пусть даны последовательности путей А/..... А„ такие, что каждая А, есть

подсеквенция Г, Тогда существует дерево вывода О 'для А в 55Ф *//■ из А¡, ,,А„ такое, что А является подсеквенцией Г.

Теорема полноты 85Ф'"|р (Обратного метода с избыточностями). Формула Ф системы Б5 невыполнима тогда и только тогда, когда пустой путь е имеет опровержение в исчислении 5'5Ф' V Доказательство последней теоремы подтверждает правомерность удаления всех

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

Далее рассматривается такой прием сокращения пространства поиска как Ф-

упорядочение. Сначала вводится отношение упорядочения на множестве всех Ф-

путей. Метод резолюции со стратегией упорядочения для классической логики

упорядочивает литеры в дизъюнктах и затем требует, чтобы правило резолюций

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

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

модальной логической системы 55. Классическое упорядочивание литер

преобразовывается для модального случая, и называется Ф-упорядочением.

Определение. Два пути называются братьями, если один из них имеет вид лли а другой - лл„ либо один имеет вид лvr, а другой - л^.

Договоренность. В дальнейшем тексте работы символом яг обозначают любой из символов л или v, символом * - любой из символов г или I; символом й любой из символов □ или й

Определение. Для заданной формулы Ф назовем Ф-упорядочением любое отношение полного порядка > на множестве всех Ф-путей, удовлетворяющее следующим условиям:

1. Я/УЛ], всякий раз когда

a) модальная длина яг/ строго больше модальной длины Л2, или

b) л1 и Л2 имеют одинаковую модальную длину, последний символ ж1 - х<¥ а последний символ я> - $ или

c) Я/ и Лг имеют одинаковую модальную длину и л2 ^ Л1 или

фесли лI и Ж2 имеют одинаковую модальную длину, и последний символ - лг,

последний символ л2 - лг. при этом неверны ава утверждения Ъ - л> или Я/ 1 я>> но л, имеет большую обычную длину, чем л2.

2. Не существует пути между двумя братьями, то есть не существует Ф-путей Щ, пг, я} таких, что Л1>Л2>-Лз и я>, л} — братья.

Поясним содержательную составляющую определения отношения порядка >-. Вначале применяются правила к формулам, большим относительно порядка >-. Кроме того, отношение х требует, чтобы заключение любого правила было меньше,

чем любая его предпосылка в мультимножественном упорядочении на секвенциях, индуцированных х. Условие 1а в определении порядка >- гарантирует, что

заключение правила вывода меньше посылки при применении правил (0), (0+), (□), (4), (5). Условие 1Ь введено для того, чтобы применение (0), (0+), (□), (4), (5) к секвенции, содержащей путь тш, не дало неполное исчисление. Условия 1с, Ы и 2

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

«Система проверки утверждений на основе модального вывода».

АЛГОРИТМ Ф-УПОРЯДОЧЕНИЯ. Для упорядочения путей предложен следующий алгоритм.

1 Первоначально М, определяется как множество путей в формуле Ф модальной длины ('.

2. Для всех М„ исключаятюследнее, делаем

2.1 пусть ли .., п„ - все пути в М„ заканчивающиеся $' 2.2разбиваем М, на М, - {я,, ..., я„} У {щ} у...У {ж„};

2.3 разбиваем М0 в М0- {е} у {£};

3. Пока существуют М, с более чем одним членом, делаем

3.1 пусть лщ и пх(г - два брата в М, такие, что леМ„

3.2 пусть N и V- множества всех префиксов соответственно из жщ и кжг;

3.3 разбиваем М,в М,- (ЫиИ)>1]уЫу{юхг}у{лщ}.

Когда алгоритм завершится,, секвенция состоит из одноэлементных множеств. В

этом случае мы допускаем, что л>-7г'; если секвенция имеет вид ...{л} >...>■ {я'} ....

Лемма Любое упорядочение, полученное алгоритмом упорядочения на формуле Ф

является Ф-упорядочением.

Следствие. Ф-упорядочение существует.

Понятие Ф-упорядочения введено для того, чтобы доказать существование опровержения в определенной форме, связанной с этим упорядочением, и поэтому оно сокращает пространство поиска вывода таких опровержений. Договоренность. Пусть я - путь, Г- секвенция путей Запись луГ сокращает утверждение, что лУл'для каждого л'из Г. Определение. (у)-вывод в

Г. ю/1 Г. пу, (у) Г, л

будем называть относящимся к Ф-упорядочению «У», если лу)УГ и лугуГ Аналогично вводится понятие (л)-вывода, относящегося к «>-». Определение. Дерево вывода в 55фра), будем называть относящимся к «у», если каждый (л) и каждый (у) вывод из этого дерева относится к «у». Лемма о существовании вывода, относящегося к «>-». Пусть Ф - невыполнимая формула и «у» - Ф-упорядочение Тогда для пустого пути е существует опровержение в которое относится к «У».

В целях исследования свойств отношения >- и доказательства теоремы полноты

для соответствующего исчисления вводится понятие «у»-компакта.

Лемма о «»-»-компактах. Пусть «у» - Ф-упорядочение. Тогда

1. посылка каждого )-вывода - «У»-компакт;

2. если Г- «у»-компактная секвенция, встречающая в дереве вывода е, то тогда каждый (ж)-вывод, имеющий Г своим заключением, относится к «У»;

3 если Г- «У»-компактная секвенция, встречающая в дереве вывода е и если Г содержит по крайней мере один у-путь или л-путь, то тогда существует (ж)-вывод, все посылки которого - «У»-компакты.

Модифицируем исчисление 55ф,*|р с учетом критерия избыточности для Ф-упорядочения.

Определение. Обозначим через 55Ф:~1р исчисление, полученное из Б5Ф1Р.

• удалением всех секвенций путей, содержащих пути различной модальной длины,

• удалением всех секвенций путей, содержащих противоречивую пару путей;

• удалением всех выводов, не относящихся к у.

В исчислении 55Ф ^[р справедливы следующие утверждения.

Лемма бимоделирования для 85Ф'^р.

/ Пусть D - дерево вывода в S5Тогда образ формул D ' для D является деревом вывода Ф в S50im ;

2 Пусть D'- дерево вывода секвенции А/, А„ в S50hn. и п>, ... л„ - такие пути, что Vi =1 ,п Тогда существует дерево вывода D для Л/, . , я„ в S50/r> такое, что D 'является образом формул дерева вывода D

3. Пункты I и 2 справедливы, если везде "дерево вывода" заменить на "опровержение "

Определение. Дерево вывода в S50ir называется относящимся к Ф-упорядочению, если выполнены следующие условия.

1 для каждого (у)-вывода этого дерева вывода

Г. яу/ Л KVr (у) Г, А, к

мы имеем iiv/>Tu nvr)~T;

2. аналогично, для каждого (л^)-вывода (соответственно (лг)-вывода) этого дерева мы имеем жл/УГ (соответственно жлг>-Г).

Лемма подсеквенциальности для 85ф,>"[1>. Пусть D - опровержение пустого пути е в S^paih, относящееся к «У» и!- вывод в De виде:

Ei^r», г

и пусть даны секвенции путей Ai, ..., А„ такие, что каждая А, есть подсеквенция Г,. Тогда существует дерево вывода D'для А в 55Ф>я> из Aj, ...,Ап такое, что А является подсеквенцией Г.

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

Лемма подсеквенциальности для деревьев вывода в SS4*'^. Пусть D -опровержение е в S50palh, относящееся к у, D"- поддерево вывода в D секвенции Г из секвенций Г/. ..., Г„ и А¡, ..., А,, - подсеквенции Г/, Г„ соответственно. Тогда существует дерево вывода D' для А в S5Ф У/Р из А/, ..., А„ такое, что А является подсеквенцией Г

Теорема полноты SS*'^. Формула Ф системы S5 невыполнима тогда и только тогда, когда пустой путье имеет опровержение в исчислении S5ф V

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

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

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

избыточными совместно с дизъюнктами, к которым они относятся. Далее

рассматривается дедуктивная система {55ф' *//>} на множестве объектов.

Отметим, что в исчислениях путей $5Фраф и 55ф№ целевым объектом является пустая секвенция е. Сформулируем теорему полноты для исчисления {55Ф| V}, то

есть для системы множественного вывода, полученного из 55ф' *)/>.

Теорема полноты для {£5*' Пусть Ф - формула логики 55

и у- Ф-упорядочение Тогда

1. если какое-либо дерево вывода в /55Ф' У1Р} успешно, то Ф невыполнима.

2. если Ф невыполнима, то любое справедливое дерево вывода в успешно Для того чтобы доказать теорему полноты для {55ф V} с предпосылкой, то есть,

что любое справедливое дерево вывода в этой системе содержит пустой путь е как только формула Ф невыполнима, определяется более строгое понятие предпосылки. Определение. Мы будем говорить, что секвенция путей П префиксно-предпосылает секвенцию путей Я' если для любого пути к ёП-П' существует

путь тг'ё П'-П такой, что ж С ж'.

Определение. Исчислением /55"® с префиксной предпосылкой называется дедуктивная система, полученная из ^55ф V/ добавлением следующего «правила префиксной предпосылки»: Ми{П, П'} >Ми{П}, где П префиксно-предпосылает П'и

п*п:

Теорема полноты для {85ф' с префиксной предпосылкой.

1.Для любого успешного дерева вывода в системе /ЗЗ0" ^¡р} с префиксной предпосылкой формула Ф логики 55 невыполнима.

\

2 Для пюбой невыполнимой формулы Ф логики 55 любое справедливое •дерево вывода М в {Б50' У1р) с префиксной предпосылкой успешно.

Общий алгоритм обратного метода установления выводимости. Укажем общий алгоритм установления выводимости, основанный на обратном методе, для произвольной формулы Ф модальной логики 55, учитывающий все выявленные стратегии сокращения пространства поиска вывода.

I этап. Строятся базовые исчисления для исходной логической системы 55 -исходное секвенциальное исчисление 55%, и обратное секвенциальное исчисление 55ф/т, для доказательства исследуемой формулы Ф.

II этап. Строятся прямое исчисление путей 55фд,,А и обратное исчисление путей 85Ф1р с целью сохранения информации о правилах вывода соответственно в исчислениях 55&9 и 55ф/т..

III этап. Поиск опровержения исходной формулы ~Ф из 55 заменяется на интуитивно более понятный поиск пустого пути £ в исчислении БЗ0^. В процессе поиска доказательства используются различные стратегии, основанные на свойствах исчислений путей и позволяющие сократить пространство поиска вывода.

IV этап. Дерево вывода пустого пути е, полученное в 55ф//>, отображается в исходную систему 55^.

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

Рассмотрена разработанная автором оболочка экспертной системы на основе классического нечеткого вывода (Ларионов Д.С., Новосельцев В.Б. Оболочка экспертной системы на основе нечетких рассуждений с прямым и обратным выводом // Математическое моделирование- 2002. - Т. 14. - № 9. - С. 48-52). Для данной оболочки указаны недостатки в виде используемых ей коэффициентов

определенности. Этим обоснована замена коэффициентов определенности на модальные операторы.

Реализованная программа «Система проверки утверждений на основе модального вывода» проверяет на выводимость предложенную ей модальную формулу. Программа написана в визуальной среде Delphi 7 0 на объектно-ориентированном языке программирования Object Pascal.

Система проверила основную гипотезу Управления актуарных расчетов Пенсионного Фонда России о том, что к 2050г. соотношение числа работающих к числу пенсионеров будет близко к единице. Эта гипотеза подтвердилась при условии роста числа пенсионеров. Тем более, эта проблема и знание данной информации полезно для Томской области, так как для нее указанный коэффициент на 2003г. равен 1,35 , что ниже общероссийского, составляющего 1,8 . Результат работы системы с данной гипотезой указан на рис. 5. Факт использования системы подтвержден соответствующим заключением.

Также программа внедрена на ОАО «Манотомь» и используется для логического анализа производственной мощности предприятия. Система анализирует движение изготовляемого продукта по всему производственному циклу от запуска до реализации, при этом учитывая связи между промежуточными звеньями процесса, такими как запуск, сборка, регулировка, ОТК, поверка, упаковка и так далее. Программа в результате своей работы указывает, при каких условиях заказ будет выполнен в срок, или обосновывает невыполнимость заказа при заданных параметрах. Опираясь на выводы системы, можно вести грамотную производственную и сбытовую политику, что, несомненно, приведет к увеличению продаж, а, следовательно, и к увеличению прибыли предприятия. Имеется соответствующее заключение о внедрении.

В заключении приведены основные выводы и результаты диссертационной работы.

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

pue. 5

Основные результаты работы

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

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

2 Рассмотрены прямое секвенциальное исчисление 55гя/ и обратное секвенциальное исчисление 55°,т, в которых будет происходить проверка на невыполнимость исходной формулы Ф. Доказана полнота данных исчислений.

3 В целях практического применения алгоритма обратной выводимости, для технического удобства программирования и сокращения пространства вывода введены прямое исчисление путей ¿'5Ф/И,/, и обратное исчисление путей 55фу/>. Аксиоматика данных исчислений непосредственно зависит от проверяемой формулы Ф, точнее от ее структуры (подформул).

4. Доказаны теоремы полноты в исчислениях 55"'^,¡, и 55ф/у>, а вместе с ними сопутствующие важные утверждения: соответствующие леммы бимоделирования для данных исчислений.

5. Были исследованы свойства построенного исчисления путей, на основании которых предложены строгообоснованные стратегии сокращения поиска вывода в системе 55.

6. Была предложена и теоретически обоснована стратегия, основанная на Ф-упорядочении, определяющая эффективную последовательность применения правил вывода к дизъюнктам из пространства поиска вывода.

7. Были предложены и теоретически обоснованы эффективные стратегии для системы Б5, подобные стратегиям предпосылки для логик К и КТ, позволяющие заметно сокращать пространство поиска вывода уже в процессе порождения дизъюнктов.

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

9. Разработана программа «Система проверки утверждений на основе модального вывода», в основе которой лежит алгоритм обратного метода установления выводимости для автоэпистемической логики и использованы методы Ф-упорядочения. Система апробирована на актуарных гипотезах Пенсионного Фонда России, в частности проверена гипотеза демографической ситуации в стране к 2050г., о чем получено соответствующее заключение. Также имеется заключение о внедрении программы на ОАО «Манотомь».

Основные публикации по теме диссертации

Larionov DS. Auto-epistemic Logic for Expert System's Inference Engine // Materials of the 9th Russian-Korean International Symposium on Science and Technology "KORUS-2005".-2005.-Vol. 1.- P. 649-652. (Ларионов Д.С. Автоэпистемическая логика для механизма вывода экспертных систем // Материалы 9-го Русско-Корейского международного симпозиума по науке и технологиям "KORUS-2005" -2005-Т. 1С. 649-652.) , Ларионов Д.С. Использование модальной логики для проектирования оболочек экспертных систем // Известия Томского Политехнического Университета. -2005. - Т. 308. -№ 4. - С. 173-177.

Ларионов Д.С, Новосельцев В.Б. Оболочка экспертной системы на основе нечетких рассуждений с прямым и обратным выводом П Математическое моделирование.- 2002.-Т. 14.-№ 9. - С. 48-52.

Ларионов Д.С. Модальная логика для механизма вывода экспертной системы // Труды XXIV Конференции молодых ученых механико-математического факультета МГУ. - 2002. -1. - С. 108-110

Ларионов Д.С. Оболочка экспертной системы с прямым и обратным выводом на основе нечетких рассуждений // Труды XXIII Конференции молодых ученых механико-математического факультета МГУ «Современные исследования в математике и механике». - 2001. - П. - С. 223-229

Ларионов Д.С. Оболочка экспертной системы на базе нечеткого вывода // Труды XXII Конференции молодых ученых механико-математического факультета МГУ «Аналитические и численные методы в математике и механике». - 2000. -I.-C. 97-101

Ларионов Д.С. Оболочка экспертной системы на основе нечетких рассуждений с прямым и обратным выводом // Материалы XXXIX международной научной студенческой конференции. - 2001. - Новосибирск, НГУ. - С. 194-195 Ларионов Д.С. Оболочка экспертных систем, поддерживающих нечеткий вывод // Материалы XXXVIII международной научной студенческой конференции. -2000. - Новосибирск, НГУ. - С. 110-111

Ларионов Д.С. Логический вывод в экспертных системах// Материалы V межвузовской конференции молодых ученых. - 2001. - Томск, ТГПУ. - С.144-149

Ларионов Д.С. Автоматическая система вывода // Материалы IV межвузовской конференции молодых ученых. - 2000. - Томск, ТГПУ. - С. 128-132

Подписано к печати 14.11 2005 г. Тираж 65 экз. Заказ № 113 Бумага офсетная. Формат 60 X 84/16. Печать RISO. Отпечатано в типографии ООО «РауШ мбХ»

Лицензия Серия ПД № 12-0092 от 03.05.2001 г 634034, г. Томск, ул. Усова 7, ком 052. тел (3822)56-44-54

РНБ Русский фонд

4306

ВВЕДЕНИЕ.

1. Актуальность задачи поиска вывода.

2. Цель работы и задачи диссертации.

3. Методы построения алгоритма и исследований.

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

5. Научная новизна и практическая ценность результатов работы.

6. Личный вклад.

7. Основные положения, выносимые на защиту.

8. Постановка задачи.

9. Обзор родственных работ.

10. Структура работы.

ГЛАВА I. ЛОГИЧЕСКАЯ СИСТЕМА Б5 (КТ45).

1.1. Синтаксис и семантика модальной логики Б5.

1.1.1. Семантика возможных миров.

1.1.2. Свойство немонотонности автоэпистемической логики.

1.1.3. Автоэпистемическая логика, ее язык, синтаксис и семантика.

1.1.4. Семантика возможных миров автоэпистемической логики.

1.2. Понятие мультимножества и исчисление секвенций для системы 85.

1.2.1. Общая схема обратного метода установления выводимости.

1.3. Прямое исчисление 855е(5 и обратное исчисление 85\,у.

1.4. Выводы по главе.

ГЛАВА II. ИСЧИСЛЕНИЕ ПУТЕЙ ДЛЯ СИСТЕМЫ 85.

2.1. Исчисление путей 85фРАтн (прямое исчисление путей).

2.2. Обратное исчисление путей 85Ф1ЫУ.

2.3. Выводы по главе.

ГЛАВА Ш. УСТРАНЕНИЕ ИЗБЫТОЧНОСТЕЙ ИСЧИСЛЕНИЯ ПУТЕЙ.

3.1. Критерии избыточности для обратного метода.

3.2. Стратегия Ф-упорядочения.

3.2.1. Алгоритм упорядочения.

3.3. Полнота обратного метода исчисления 85% без секвенций, не относящихся к«>-».

3.4. Предпосылка как критерий избыточности.

3.5. Общий алгоритм установления выводимости.

3.6. Выводы по главе.

ГЛАВА IV. ПРИМЕНЕНИЕ ОБРАТНОГО МЕТОДА УСТАНОВЛЕНИЯ ВЫВОДИМОСТИ ДЛЯ МЕХАНИЗМА ВЫВОДА ЭКСПЕРТНЫХ СИСТЕМ.

4.1. Пример оболочки экспертной системы на основе классического нечеткого вывода.

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

4.2.1. Оценка актуарных гипотез ПФР.

4.2.2. Анализ производственной мощности предприятия.

4.3. Выводы по главе.

В последнее время интенсивно рассматриваются вопросы автоматизации процессов получения решений компьютерными программами - это связано не только с классическими задачами искусственного интеллекта доказательства теорем и построения советующих экспертных систем, но и с бурным развитием и внедрением в производственный процесс корпоративных информационных ERP-систем, CRM-систем [www.expert-systems.com], программ управления технологическими процессами, задач извлечения данных и знаний: анализ данных, анализ документов, поиск по смыслу в Internet, распознавание текста и так далее [9]. Несмотря на то, что для решения указанных вопросов успешно применяются такие технологии, как нейронные сети, семантические сети и фреймы, набирает рост и интерес к традиционному логическому методу хода рассуждений за счет привлечения неклассических модальных логик. Наличие большого числа эвристик в рассуждениях соответствующих систем, их неспособность всегда четко обосновать свое решение ставят под сомнение применение нелогических способов рассуждений. В свою очередь, вывод, опирающийся на одну из модальных логик, сохраняет строгость и обоснованность классических аксиоматических систем вывода, однако при этом он гибок за счет наличия операторов □ (необходимости) и 0 (возможности). Так же многие модальные логики обладают свойством немонотонности, позволяющим пересматривать свои выводы в процессе рассуждения.

В частности, проблему построения доказательства заданного целевого утверждения для экспертной системы можно свести к проблеме поиска вывода формул определенного логико-математического языка в соответствующем исчислении. Для теорий, основанных на классической логике, исходным пунктом в решении проблемы поиска вывода является, как правило, решение проблемы поиска вывода в исчислении предикатов первого порядка, на базе которого (добавляя те или иные аксиомы и правила вывода) осуществляется формализация различных математических теорий. Имеются многочисленные работы как в области теории логического вывода в классическом исчислении предикатов и теории разрешимых фрагментов этого исчисления, так и в области практического построения алгоритмов программ автоматического поиска вывода. Для автоматизации доказательства недостаточно решить удовлетворительно проблему автоматического поиска вывода в исчислении предикатов, особенно в случае, когда соответствующее теории исчисление имеет дополнительные правила вывода. Такой случай имеет место, например, при задании исчисления с равенством путем добавления не только аксиом, но и правил для равенства. Для успешной формализации желательно, чтобы методика построения алгоритмов автоматического поиска вывода допускала распространение на различные системы. Один из успешных примеров реализации такого алгоритма, реализующего обратный метод установления выводимости для модальной логики КТ, описан в работе В.В. Бурлуцкого [6]. В нем используется логика знаний, где оператор □ интерпретируется как «известно».

Рассмотрим основные подходы для модифицируемых рассуждений. К основным семействам немонотонных логик [33], [34], [7] можно отнести:

• Логики умолчаний [72]. Они позволяют формализовать модифицируемые рассуждения с помощью правил вывода, присущих области применения. Эти знания выражают правила вида «большинство птиц летает» в форме «если непротеворечив (выполним) вывод, что некая отдельная птица может летать, то она летает». Здесь есть возможность выражать правила с исключениями, не перечисляя сами эти исключения.

• Модальные немонотонные логики Мак-Дермотта [62], [63]. Эти логики базируются на аксиоматических системах модальной логики и предназначены для характеризации множеств взаимно «выполнимых» утверждений, которые можно вывести из какого-то задаваемого множества посылок.

• Автоэпистемические логики [67], [68], [69]. Это реконструкция немонотонных логик Мак-Дермотта. Взяв какую-либо систему модальной логики, предполагают, что некий идеально разумный агент рассуждает интроспективным образом в рамках выбранной системы и на основе своих собственных предположений. Рассуждения, проводимые агентом, являются модифицируемыми, ибо относятся к определенному состоянию знаний, которое может оказаться изменчивым. Хотя автоэпистемические логики и логики умолчаний создавались для различных применений, их выразительные возможности часто бывают равносильными [55].

Особо стоит отметить подходы через минимизацию [34], предназначенные для формализации модифицируемых рассуждений и естественно вписывающиеся в рамки классической логики. Вывод в таких системах основан на минимизационных соглашениях для стратегии обращения к неизвестным сведениям. Будучи примененным к базам данных, содержащим только сведения в элементарной логической форме, такое соглашение состоит в опровержении все еще незаписанной информации; истинной предполагается информация, явно присутствующая в базе данных, а вся остальная позитивная информация считается ложной. При обобщении на базы знаний эти соглашения состоят в более громоздких условиях минимальности, связанных с множествами определенных сущностей, удовлетворяющих некоторым формулам данной базы знаний. В качестве указанных минимизационных соглашений могут служить гипотеза замкнутого мира [71], [73], [75], [76], которая формулируется в виде принципов и методов, позволяющих управлять запросами базы знаний немонотонным образом по отношению к эволюции содержимого этой базы. Соглашения могут также принимать вид аксиом или схем аксиом, которые должны быть добавлены к рассматриваемой базе знаний, например, аксиом пополнения [57], [75], [76], [77] или аксиом очерчивания [60], [61] [58], [59]. В логическом программировании, например, в языке Пролог [5], [32], [1] специальные операторы аппроксимируют логическое отрицание с помощью некоторой конечной процедуры отрицания через неудачу [34], [57], [77]. Эти операторы позволяют доказать модифицируемым образом, что некое утверждение нельзя вывести на основе знаний, имеющихся в логической программе. В наиболее общем виде минимизационные соглашения представляются различными операциями разграничения областей истинности предикатов и формул из базы знаний, а также разграничения множеств и областей констант и функций этой базы. Эти операции взаимодействуют согласно определенным приоритетам и являются выразителями специфической рациональности рассуждающего агента

44], [34].

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

4.3. Выводы по главе

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

Одна из реализаций обратного метода установления выводимости в виде «Системы проверки утверждений на основе модального вывода» показывает то, что особую пользу метод приносит в системах прогнозирования и проверки гипотез. По факту в системе используется комбинированный вывод, то есть движение по дереву вывода не только от аксиом к целевой гипотезе, но и в обратном направлении. Такой прием, особенно в сочетании с Ф-упорядочением наиболее эффективен.

Заключение

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

1. Была сформулирована и теоретически обоснована оригинальная разрешающая процедура для автоэпистемической системы £5 - одной из самых выразительных и полных модальных логик.

2. Был сформулирован и теоретически обоснован интуитивно ясный и наглядный алгоритм поиска вывода для системы 5*5, который опирается на формализацию обратного метода, основанную на исчислении путей.

3. Были исследованы свойства построенного исчисления путей, на основании которых предложены строгообоснованные стратегии сокращения поиска вывода в системе ¿>5.

4. Была предложена и теоретически обоснована стратегия, основанная на Ф-упорядочении, определяющая эффективную последовательность применения правил вывода к дизъюнктам из пространства поиска вывода.

5. Были предложены и теоретически обоснованы эффективные стратегии для системы подобные стратегиям предпосылки для логик К и КТ, позволяющие заметно сокращать пространство поиска вывода уже в процессе порождения дизъюнктов.

6. Было проведено строгое доказательство теоремы полноты для исчисления путей системы 5*5 с учетом всех вышеназванных стратегий.

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

118 различного уровня. Предложенные алгоритмы удовлетворяют принятым современным критериям эффективности. Они были критически сопоставлены с различными традиционными методами поиска вывода.

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

1. Было проведено глубокое исследование базовых исчислений обратного метода системы Я5 и соответствующих им исчислений путей.

2. Был детально описан и теоретически обоснован механизм вывода для экспертной системы, база знаний которой формализована с помощью одного из самых семантически богатых языков модальной логики 55.

3. Были предложены эффективные и технически легко реализуемые стратегии для системы £5, сокращающие пространство поиска вывода уже в процессе пополнения базы данных дизъюнктов.

4. Реализована программа «Система проверки утверждений на основе модального вывода», показывающая, что особую пользу метод приносит в системах прогнозирования и проверки гипотез.

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

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

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

Одна из реализаций обратного метода установления выводимости в виде «Системы проверки утверждений на основе модального вывода» показывает то, что особую пользу метод приносит в системах прогнозирования и проверки гипотез. По факту в системе используется комбинированный вывод, то есть движение по дереву вывода не только от аксиом к целевой гипотезе, но и в обратном направлении. Такой прием, особенно в сочетании с Ф-упорядочением, наиболее эффективен.

1. Адаменко А.Н., Кучу ков A.M. Логическое программирование и Visual Prolog.-СПб.: БХВ-Петербург, 2003. 992с.: ил.

2. Алексеева Е.Ф., Стефанюк В.Л. Экспертные системы (состояние и перспектива) // Известия АН СССР. Техническая кибернетика. 1984. -№5. - С. 153-167.

3. Барвайс Дж. Справочная книга по математической логике. М.: Наука. -1983.

4. Боброва Т.Ю., Горшкова Н.В., и др. Краткий актуарный сборник. М.: Современная экономика и право. - 88 с.

5. Братко И. Программирование на языке Пролог для искусственного интеллекта: М.: Мир, 1990. 560 е., ил.

6. Бурлуцкий В.В. Реализация обратного метода установления выводимости для модальной логики KT. Диссертация на соискание ученой степени кандидата физико-математических наук. 05.13.01. -Томск, 2001.

7. Вагин В.Н., Головина Е.Ю., Загорянская A.A., Фомина М.В. Достоверный и правдоподобный вывод в интеллектуальных системах. М.: ФИЗМАТЛИТ, 2004. - с. 704

8. Воронков A.A. Метод поиска доказательства// Вычислительные системы. Новосибирск. 1985. - т. 107

9. Гаврилов A.B. Гибридные интеллектуальные системы.-Новосибирск: Изд-во НГТУ, 2003.-164 с.

10. Гнеденко Б. В. Курс теории вероятностей: Учебник Изд. 6-е, - М.:Наука. Гл. ред. физ.-мат. лит., 1988. - 448 с.

11. Давыдов Г.В., Маслов С.Ю. и др. Машинный алгоритм установления выводимости на основе обратного метода// Записки ЛОМИ АН СССР. 1969. -т. 16. -С.8-20

12. Драгалин А.Г. Математический интуиционизм. Введение в теорию доказательств. М.:Наука. - 1979.

13. Ларионов Д.С. Модальная логика для механизма вывода экспертной системы// Труды XXIV Конференции молодых ученых механико-математического факультета МГУ. 2002. -1.-е. 108-110

14. Ларионов Д.С. Оболочка экспертной системы на базе нечеткого вывода// Труды XXII Конференции молодых ученых механико-математического факультета МГУ «Аналитические и численные методы в математике и механике». -2000.-I.-c. 97-101

15. Ларионов Д.С. Использование модальной логики для проектирования оболочек экспертных систем // Известия Томского Политехнического Университета. 2005. - Т. 308. - № 4. - С. 173-177.

16. Larionov D.S. Auto-epistemic Logic for Expert System's Inference Engine // Materials of the 9th Russian-Korean International Symposium on Science and Technology "KORUS-2005".-2005.-Vol. 1.- C. 649-652

17. Ларионов Д.С., Новосельцев В.Б. Оболочка экспертной системы на основе нечетких рассуждений с прямым и обратным выводом // Математическое моделирование.- 2002. Т. 14. - № 9. - С. 48-52.

18. Марселус Д. Программирование экспертных систем на Турбо Прологе: Пер. с англ. М.: Финансы и статистика, 1994. - 256 е.: ил.

19. Мае лов С.Ю. Обобщение обратного метода на исчисление предикатов с равенством// Записки ЛОМИ АН СССР. 1971. - т.20. - С.80-96

20. Маслов С.Ю. Обратный метод установления выводимости в классическом исчислении предикатов.-ДАН СССР, Т. 159, № 1, 1964.-С. 17-20.

21. Маслов С.Ю. Обратный метод установления выводимости для логических исчислений-Труды Мат.института АН СССР, Т.98, 1968.-С. 26-87.

22. Маслов С.Ю. Обратный метод установления выводимости для непредваренных формул исчисления предикатов// ДАН СССР. 1967. - №1. -С. 22-25.

23. Маслов С.Ю. О поиске вывода в исчислениях общего типа.-Зап. науч. семинаров.-ЛОМИ АН СССР, Т.32, 1972.- С. 59-65.

24. Маслов С.Ю. Применение обратного метода к теории разрешимых фрагментов классических исчислений// ДАН СССР. 1966. - №1. - С. 17-20.

25. Маслов С.Ю. Связь между тактиками обратного метода и метода резолюций// Записки ЛОМИ АН СССР. 1969. - т.16. - С.21-26

26. Мендельсон Э. Введение в математическую логику. М.: Наука. - 1976.

27. Минц Г.Е. Резолютивные исчисления для неклассических логик//9-ый Советский Кибернетический симпозиум, М.: ВИНИТИ. 1981.- т.2. - С.34-36

28. Попов Э. В. Экспертные системы: Решение неформализованных задач в диалоге с ЭВМ. М.: Наука. Гл. ред. физ.-мат. лит., 1987.-288 с.

29. Соловьев А. К. Актуарные расчеты в пенсионном страховании. -М.: Финансы и статистика, 2005.-240 е.: ил.

30. Стерлинг Л., Шапиро Э. Искусство программирования на языке Пролог: М.: Мир, 1990.-235 е., ил.

31. Тейз А., Грибомон П., Ж. Луи и др. Логический подход к искусственному интеллекту, т.1 От классической логики к логическому программированию-М.: Мир, 1990.

32. Тейз А., Грибомон П., Юлен Г. и др. Логический подход к искусственному интеллекту, т.2 От модальной логики к логике баз данных.-М.: Мир, 1998.

33. Уотермен Д. Руководство по экспертным системам: Пер. с англ. М.: Мир, 1989.-388 е., ил.

34. Фейс Р. Модальная логика. М.: Наука. - 1974.

35. Чень Ч., Ли Р. Математическая логика и автоматическое доказательство теорем.-М.: Наука, 1983.

36. Bachmair L. Gansinger Н. Resolution theorem proving// Handbook of Automated reasoning, Robinson A. And Voronkov A. Eds. Elsevier science and MIT Press. 2000.

37. Borger E., Grader E. and Gurevich Y. The Classical Decision Problem, Springer Verlag 1997

38. Davis M. Eliminating the Irrelevant from Mechanical Proofs// Proc. Symp. On Experimental Arithmetic, Chicago, 1962.

39. Degtyarev A. And Voronkov A. Equality elimination for the inverse method and extension procedures// Proc. International Joint Conference on Artificial Intelligence (IJCAI), C. Mellish ed., Montreal. 1995. - vol.1. - pp.342-347

40. Fitting, M. Proof methods for modal and intuicionistic logics// Synthese Library, Reidel Pub. Comp. 1983. - vol. 169.

41. Friedman J.A. Semi-decision procedure for the functional calculus// Journal of ACM.- 1963.-vol. 10, №1.-pp.1-25

42. Gelfond M. On stratified autoepistemic theories, Proc. AAAI-87, pp. 207-211, 1987.

43. Gentzen, G. Untersuchungen über das logische Schliesen// Mathematical Zeitschrift-39. 1934. - pp. 176-210, 405-431

44. Giuchinglia F. et al. SAT-based decision procedures for classical modal logics// Journal of automated reasoning. 1999. - To appear in the Special Issues: Satisfiability at the start of the year 2000. (SAT 2000)

45. Goldblatt, R. Logics of time and Computation// Lecture Notes, Center for the Study of Language and Information. 1987. - №7

46. Herbrand J. Recherches sur la theorie de la demonstration. Warsaw, 1930.

47. Horrocks I., Patel-Schneider P., Sebastiani R. An analysis on empirical testing for modal decosion procedures// Logic Journal of the IGPL 2000 - vol. 8, №3 - pp. 293323.

48. HustadtU. and ShmidtR. On evaluating decision procedures for modal logic// IJCAI-97. 1997. - vol.1. - pp.202-207

49. Jackson P. Introduction to Expert Systems. Addison Wesley, 1999.

50. Kleene S. C. Introduction to Mathematics, North-Holand, Amsterdam, 1952.

51. Konolige K. On the relation between default theories and auto-epistemic logic. Proc. IJCAI-87, pp. 394-401, 1987.

52. Kripke S.A. Semantical considerations on modal logic// Reference and Modality, Oxford University Press, London. 1971. - pp. 63-72

53. Kuken K. Negation in logic programming, J. Logic Programming, vol. 4, no. 4, pp. 289-308, 1987

54. Lifschitz V. Computing circumscription, Proc. IJCAI-85, pp. 121-127, 1985.

55. Lifschitz V. Pointwise circumscription: preliminary report, Proc. AAAI-86, pp. 406-410, 1986.

56. McCarthy J. Circumscription: a form of non-monotonic reasoning, Artificial Intelligence, vol. 13, no. 1-2, pp. 27-39, 1980.

57. McCarthy J. Applications of circumscription to formalizing common-sense knowledge, Artificial Intelligence, vol. 28, pp. 89-116, 1986.

58. McDermott D. and Doyle J. Non-Monotonic logic 1 // Artificial Intelligence. -1980. V. 13. - № 1-2. - P. 41-72.m 63. McDermott D. Non-monotonic logic 2: non-monotonic modal theories // J. ACM. -1982.-V. 29.-№ l.-P. 34-57.

59. Mints G. Resolution calculus for the first order linear logic// Journal of Logis, Language and Information. 1993. - №2. - pp.58-93

60. Mints G., Orevkov V. And Tammet T. Transfer of sequent calculus strategies to resolution for S4// Proof Theory of Modal logic. Studies in Pure and Applied logic, Kluwer Academic Publishers. 1996m

61. Mints G., Voronkov A. And Degtyarev A. Inverse method.// Handbook of Automated reasoning, Robinson A. And Voronkov A. Eds. Elsevier science and MIT Press. 2000

62. Moore R.C. Possible-world semantics for auto-epistemic logic // Proc. AAAI-Workshop on Non-Monotonic Reasoning. October 1984. - New Paltz, N.Y., 1984. -P. 344-354.

63. Moore R.C. Semantical considerations on non-monotonic logic // Artificial Intelligence. 1985. - V. 25. - № 1. - P. 75-94.

64. Moore R.C. Autoepistemic logic // Non-Standart Logics for Automated Reasoning (P. Smets et al., eds.). 1988. - P. 105-136.

65. Reuter R. A logic for default reasoning. Artificial Intelligence, vol. 13, no 1-2, pp. 81-131, 1980

66. Reiter R. On closed-world data base, in H. Gallaire and J. Minker (editeurs), Logic and Data Bases, Plenum Press, New York, pp. 55-76, 1978.

67. Robinson J.A. On automatic deduction// Rice Univ. Studies. 1964. - vol.50, №1. - pp. 69-89.

68. Shepherdson J.C. Negation as failture: a comparison of Clark's completed data base and Reiter's closed closed world assumption, J. Logic Programming, vol. 1, no. 1, pp. 51-79, 1984.

69. Shepherdson J.C. Negation as failture II, J. Logic Programming, vol. 2., no. 3, pp. 185-202, 1985.

70. Shepherdson J.C. Negation in logic programming, in J. Minker (editeur), Foundations of Mathematics, vol. 124, pp. 277-318, North-Holland, Amsterdam, 1988.

71. Stalnaker R. A note on non-monotonic modal logic, Dep. of Philosophy. Cornell University, Ithaca, New York, juin, 1980.

72. Tachella A. *SAT system description// Proceedings of the 1999 International Description Logic Workshop (DL'99), P.Lambrix, A.Borgida, M.Lenzerini, R.Moller and P.Pattel-Schneider, Eds. CEUR-WS. 1999. - vol.22. - pp. 142-144

73. Tammet T. Proof strategies in linear logic// Journal of automated reasoning. -1994. vol. 12, №3. - pp.273-304

74. Tammet T. Resolution theorem prover for intuitionistic logic// CADE-13, M.McRobbie and J.Slaney, Eds. Lecture Notes in Computer Science 1996. -vol.1104.-pp.2-16

75. Voronkov, A. K-inverse-K: a theorem prover for K// Automated Deduction. CADE-16, International Conference on Automated Deduction, H.Ganzinger Eds. Lecture Notes in Artificial Intelligence. 1999. - vol.1632, Springer Verlag. - pp.383387

76. Voronkov A. How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi// LICS'2000

77. Voronkov A. Theorem-proving in non-standard logic based on the inverse method// 11th International Conference on Automated Deduction, D. Kapur ed. Lecture Notes in Artificial Intelligence. 1992. - vol.607, Springer Verlag. - pp.648-662

78. Voronkov A. How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi// ACM Transactions and Computational logic.-2001.-vol. 1.- pp. 1-35

79. Wallen, L. Automated deduction in nonclassical logics. The MIT Press. - 1990 1982.-V. 29.-№ l.-P. 34-57.

80. Weidenbach et al. SPASS & FLOTTER version 0.42//CADE-13, M.McRobbie and J.Slaney, Eds. Lecture Notes in Artificial Intelligence. 1996. - vol.1104, Springer Verlag.-pp. 141-1451. Утверждаю»

81. Управляющий ГУ-ОПФР по Томской области

82. В Отделении ПФР по Томской области используется «Система проверки утверждений на основе модального вывода», разработанная Д.С. Ларионовым.

83. Логический вывод программы основан на следующих компонентах:1. автоэпистемических модальных рассуждениях;2. обратном методе выводимости;3. стратегии Ф-упорядочения формул.

84. На ОАО «Манотомь» внедрена программа «Система проверки утверждений на основе модального вывода», разработанная Д.С. Ларионовым.