Разработка метода и системы логического вывода модифицируемых заключений

• Автор: Томчук, Максим Николаевич
• Шифр специальности: 05.13.01
• Научная степень: Кандидатская
• Год защиты: 2009
• Место защиты: Пенза
• Количество страниц: 172 с. : ил.

ОГЛАВЛЕНИЕ
Введение.

Глава 1. Анализ методов и машин логического вывода и систем обработки знаний

1.1 Методы и машины логического вывода

1.1.1 Классификация видов логического вывода

1.1.2 Классификация методов логического вывода

1.1.3 Метод деления дизъюнктов

1.1.4 Машины логического вывода.

1.2 Системы обработки знаний СОЗ

1.2.1 Определение и структура.

1.2.2 Классификация.

1.2.3 Режимы функционирования.
1.2.4 Оценка эффективности
1.3 Выводы но главе 1.
Глава 2. Разработка метода логического вывода модифицируемых заключений
2.1 Формальные системы
2.2 Постановка задачи логического вывода
2.3 Расширение формулы заключения.
2.3.1 Унификация литералов
2.3.2 Согласование решений
2.3.3 Согласование значений общих переменных в конъюнкциях дизъюнктов.
2.3.4 Частичное деление дизъюнктов
2.3.5 Полное деление дизъюнктов.
2.3.6 роцедура вывода.
2.3.7 Построение абдуктивных объяснений.
2.3.8 Метод параллельного вывода с расширением формулы заключения
2.4 Минимизация формулы заключения
2.4.1 Процедура минимизации заключения
2.4.2 Метод минимизации заключения
2.5 Выбор вариантов модификации.
2.6 Особенности вывода в исчислении высказываний
2.7 Пример вывода.
2.8 Выводы по главе 2.
Глава 3. Разработка системы логического вывода модифицируемых заключений
3.1 Структура системы логического вывода
3.1.1 Обобщенная структура системы
3.1.2 Детализованная структура системы
3.2 Режимы работы системы логического вывода
3.2.1 Режим вывода модифицируемых заключений
3.2.2 Режим дедуктивного вывода.
3.2.3 Режим абдуктивного вывода.
3.2.4 Режим настройки.
3.2.5 Режим непосредственного доступа к базам знаний
3.2.6 Создание базы знаний
3.3 Машина логического вывода модифицируемых заключений.
3.4 Язык декларативного логического программирования
3.4.1 Структура логической программы
3.4.2 Идентификаторы и константы
3.4.3 Комментарии
3.4.4 Пример логической программы
3.5 Оценка эффективности систем логического вывода.
3.5.1 Критерии оценки эффективности
3.5.2 Расчет времени вывода
3.5.3 Расчет степени модификации заключения
3.6 Выводы по главе 3
Глава 4. Применение систем логического вывода модифицируемых заключений.
4.1 Области применения.
4.2 Интеллектуальные обучающие системы.
4.3 Экспертные системы.
4.4 Интеллектуальное управление вычислительными процессами
4.5 Модуль логического вывода модифицируемых заключений
4.5.1 Общая характеристика разрабатываемого программного
обеспечения
4.5.2 Структура модуля вывода
4.5.3 Язык описания базы знаний и заключения.
4.5.4 Реализация блоков модуля.
4.6 Учебная программа логического вывода ЛогикаВ
4.6.1 Структура программы
4.6.2 Язык описания исходных данных
4.6.3 Интерфейс пользователя.
4.6.4 Пример использования программы
4.7 Выводы по главе 4
Заключение.
Список сокращений
Библиографический список.
Приложения.
ВВЕДЕНИЕ
Данная диссертационная работа посвящена разработке нового метода логического вывода модифицируемых заключений на знаниях, представленных в виде формул исчисления высказываний и исчисления предикатов первого порядка, а также системы лог ического вывода модифицируемых заключений. Рассматриваются вопросы построения систем обработки знаний и машин логического вывода, использующих данный метод, в том числе особенности их программной реализации на современных параллельных вычислительных платформах. риводятся области возможного применения данного метода логического вывода, рассматривается применение логического вывода модифицируемых заключений для интеллектуального управления вычислительными процессами, в обучающих системах и в экспертных системах.
Актуальность


Полученные теоретические и практические результаты использованы в НИР «Теория и применение логического вывода с модификацией заключений» (грант Министерства Образования РФ Е-2. НИР «Разработка среды декларативного логического программирования для кластерной вычислительной системы» (ВятГУ, НИР №2). Учебная программа логического вывода внедрена в учебный процесс в Вятском государственном и Вятском государственном гуманитарном университетах. Апробация работы. Основные положения и результаты исследования докладывались и обсуждались на 5-й международной конференции «Interactive Systems: The Problems of Human-Computer Interaction» («Интерактивные системы: Проблемы взаимодействия человек - компьютер»), Ульяновск, УлГТУ, ; 9-й «Национальной конференции по Искусственному Интеллекту КИИ-», Тверь, ; Всероссийской ежегодной научно-технической конференции ВятГУ «Наука-iфоизводство-технологии-экология», Киров (,, гг. Публикации. Результаты исследования представлены в работах, из них статей, 2 тезисов докладов. Четыре работы опубликованы в научных изданиях, рекомендуемых ВАК для опубликования основных научных результатов диссертации (три работы в российских изданиях и одна в зарубежном). Структура и объем исследования. Диссертационная работа состоит из введения, четырех глав, заключения, списка сокращений, библиографического списка (включающего 3 наименования) и 2 приложений. Основная часть работы изложена на 0 страницах и содержит рисунка и 5 таблиц. ГЛАВА 1. Можно выделить несколько основных видов логического вывода. Их классификация приведена на рисунке 1. Рисунок 1. Традиционно выделяют три основных вида логического вывода: дедуктивный вывод, индуктивный вывод, абдуктивный вывод. Дедуктивный логический вывод, предполагает применение общих правил к частным случаям с выводом результата. Задачей дедуктивного вывода может являться как установление факта выводимости заданного логического выражения (заключения) из базы исходных посылок, так и поиск последовательности секвенций, необходимых для вывода заключения (построение схемы вывода). Суть дедуктивного вывода можно проиллюстрировать следующим известным примером. МСЖТАЦБОСЯАТ). Задачей дедукции является вывод цели в) из исходных посылок а) и б). В данном примере результат дедуктивного вывода положительный: заключение выводится из исходных посылок. Особенностью дедуктивного вывода в исчислении предикатов можно считать получение в результате вывода подстановок: если в выводимом заключении есть переменные, часть из них может быть заменена константами, функторами или другими переменными. SOCRAT. При этом возможно несколько вариантов подстановок. Если дополнить базу исходных посылок фактом HUMAN(PLATON), то при выведении цели MORTAL(x) на место переменной может быть подставлена любая из констант: SOCRAT или PLATON. Дедуктивный вывод относится к достоверным видам вывода. Индуктивный вывод предполагает анализ посылок и цели, на основании которых синтезируются правила. Для предложенного примера это будет означать вывод главной посылки а) из второстепенной посылки б) и заключения в). Полноценный индуктивный вывод возможен только в исчислении предикатов, поскольку понятие общих правил неприменимо к логике высказываний. Однако индуктивный вывод в логике высказываний с успехом заменяется абдуктивным выводом. Индуктивный вывод является правдоподобным, поскольку не всегда на основании набора фактов удается установить корректные закономерности. В связи с этим возникает проблема при пополнении базы знаний. Если в результате индуктивного вывода к посылкам было добавлено правило, оказавшееся впоследствии не вполне корректным, возникает задача поиска данного правила и его модификации или удаления, поскольку простое формирование новых правил или фактов с добавлением их к множеству исходных посылок сделает это множество противоречивым. В данном случае требуется применение специфического вывода с модификацией правил. Лбдуктивный вывод служит для выведения второстепенных посылок из главных посылок и заключения. Для предложенного примера это означает вывод второстепенной посылки б) из главной посылки а) и заключения в).