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

• Автор: Ларионов, Дмитрий Сергеевич
• Шифр специальности: 05.13.01
• Научная степень: Кандидатская
• Год защиты: 2005
• Место защиты: Томск
• Количество страниц: 148 с.

ОГЛАВЛЕНИЕ
ВВЕДЕНИЕ.

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

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

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

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

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

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

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

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

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

. Структура работы.
ГЛАВА I. ЛОГИЧЕСКАЯ СИСТЕМА КТ.
1.1. Синтаксис и семантика модальной логики Б5.
1.1.1. Семантика возможных миров
1.1.2. Свойство немонотонности автоэнистемичсской логики
1.1.3. Автоэпнстемическая логика, ее язык, синтаксис и семантика
1.1.4. Семантика возможных миров автоэиистемнческой логики
1.2. Понятие мультимножества и исчисление секвенций для системы Б5.
1.2.1. Общая схема обратного метода установления выводимости
1.3. Прямое исчисление БЗбер и обратное исчисление фМу.
1.4. Выводы по главе.
ГЛАВА II. ИСЧИСЛЕНИЕ ПУТЕЙ ДЛЯ СИСТЕМЫ
2.1. Исчисление путей фрАТн прямое исчисление путей.
2.2. Обратное исчисление путей фу.
2.3. Выводы по главе.
ГЛАВА Ш. УСТРАНЕНИЕ ИЗБЫТОЧНОСТЕЙ ИСЧИСЛЕНИЯ ПУТЕЙ .
3.1. Критерии избыточности для обратного метода
3.2. Стратегия Фупорядочения
3.2.1. Алгоритм упорядочения
3.3. Полнота обратного метода исчисления фр без секвенций, не относящихся
3.4. Предпосылка как критерий избыточности.
3.5. Общий алгоритм установления выводимости.
3.6. Выводы по главе.
ГЛАВА IV. ПРИМЕНЕНИЕ ОБРАТНОГО МЕТОДА УСТАНОВЛЕНИЯ ВЫВОДИМОСТИ ДЛЯ МЕХАНИЗМА ВЫВОДА ЭКСПЕРТНЫХ СИСТЕМ
4.1. Пример оболочки экспертной системы на основе классического нечеткого
вывода.
4.2. Практической применение обратного метода установления выводимости для автоэпистемичекой логики
4.2.1. Оценка актуарных гипотез ПФР.
4.2.2. Анализ производственной мощности предприятия.
4.3. Выводы по главе
ЗАКЛЮЧЕНИЕ.
СПИСОК ИСПОЛЬЗОВАННЫХ ИСТОЧНИКОВ


Такая трактовка оператора ? В связи с этим возникает актуальная проблема реализации разрешающей процедуры, основанной на обратном методе, для автоэпистемической логики. В настоящее время уже существуют ряд программ автоматического поиска доказательства, в основе большинства из которых лежат традиционные методы резолюций, семантических таблиц, а также различные их модификации. Лучшие из этих систем, такие как *БАТ или ЭЬР, ориентированы на тот или иной класс формул; они постоянно улучшаются путем добавления различных стратегий и эвристик, что позволяет говорить об их практической применимости. Программы автоматического поиска доказательства, основанные на обратном методе, начали интенсивно разрабатываться лишь в последние несколько лет, однако уже сейчас они успешно конкурируют с традиционными, о чем говорят результаты экспериментов проведенных с системой К []. Проблема построения механизма вывода для экспертных систем (ЭС), прежде всего, связана с наличием неопределенности в фактах, используемых системой. ЭС с прямым и обратным выводом, использующая коэффициенты определенности относительно фактов, с которыми она работает; имеется также ее реализация на языке логического программирования Visual Prolog, более подробно с которым можно познакомиться в [1]. Применение коэффициентов определенности можно заменить математически обоснованным выводом с применением модальной логики, хотя в ее контексте, в противовес классической логике, понятие общезначимости зачастую заменяется понятием выполнимости, что обусловлено попыткой модальной логики формализовать эволюционирующие рассуждения немонотонного типа. Для этого следует построить алгоритм обратного метода установления выводимости, основанного на автоэпистемической логике. Также следует практически реализовать указанный метод в виде программного модуля. Исследование синтаксиса и семантики автоэпистемической логики, а также ее свойств: полноты, легальности, устойчивости и т. Построение исходного секвенциального исчисления, обратного исчисления секвенций автоэпистемической логики, а также доказательства соответствующих теорем полноты - ключевого свойства любой аксиоматической системы вывода, гарантирующего корректность вывода. Доказательство соответствующих теорем полноты. Формулировка общего алгоритма установления выводимости. Практическая реализация указанного выше алгоритма и демонстрация его использования. При построении алгоритма установления выводимости, исследований свойств построенных исчислений, разработке программного обеспечения использованы методы теории классической логики высказываний и предикатов первого порядка, теории немонотонных модальных логик, теории вероятности, теории множеств и мультимножеств, теории графов, теории алгоритмов, теории объектно-ориентированного проектирования и программирования. Девятый Российско-Корейский международный симпозиум по науке и технологиям (The Eights Korea-Russian International Symposium on Science and Technology) «KORUS » (г. Новосибирск, НГТУ, июня - 2 июля г. Истра, РОССИЯ, Московский авиационный институт (Технический университет) 2-7 июля г. XXIII Конференция молодых ученых механико-математического факультета МГУ им М. В.Ломоносова (г. Москва, МГУ, 9- апреля г. XXII Конференция молодых ученых механико-математического факультета МГУ им М. В.Ломоносова (г. Москва, МГУ, - апреля г. XXXVIII Конференция «Научно-технический прогресс» (г. Новосибирск, НГУ, 2-5 апреля г. IV межвузовская конференция аспирантов и молодых ученых «Наука и образование» (г. Томск, ТГПУ, - апреля г. III межвузовская конференция «Математика: ее содержание, методы и значение» (г. Томск, ТГУ, - апреля г. Приложение 6). Реализация алгоритма обратного метода установления выводимости для автоэпистемической логики согласно общей схеме указанного метода для неклассических логик. Доказательство фундаментального свойства полноты соответствующих исчислений. Построение исчислений путей для автоэпистемической логики. Доказательство фундаментального свойства полноты соответствующих исчислений.