Реализация обратного метода установления выводимости для модальной логики КТ

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

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

Актуальность задачи поиска вывода для неклассических логик

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

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

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

ГЛАВА I. ОБЩАЯ СХЕМА ОБРАТНОГО МЕТОДА ДЛЯ ЛОГИЧЕСКОЙ СИСТЕМЫ КТ

1.1. Вводны Е ЗАМЕЧАНИЯ

1 Л.1. Семантика и синтаксис модальной логики знания 1.1.2. Мультимножества и исчислен и е секвен щи

1.2. Общая схема метода

1.3 Прямое и обратное исчисления секвенций для логики знания

ГЛАВА II. ИСЧИСЛЕНИЕ ПУТЕЙ
2.1. Прямое исчисление путей
2. 2. Обратное исчисление путей
ГЛАВА III. АНАЛИЗ ИЗБЫТОЧНОСТЕЙ
3.1. Свойства исчисления путей
3.2. Теорема полноты обратного метода с критериями избыточности
3.3. ФУПОРЯДОЧЕНИЕ
3.4. Теорема полноты обратного метода для обратного ИСЧИСЛЕНИЯ ПУТЕЙ БЕЗ СЕКВЕНЦИЙ, ОТНОСЯЩИХСЯ К
3.5. Предпосылка
3.6. Общий алгоритм установления выводимое ти
ЗАКЛЮЧЕНИЕ
ЛИТЕРАТУРА


В результате процесс удлиняется (экспоненциально) и для доказательства сравнительно простых утверждений требуется слишком много машинного времени. Указанная проблема решается введением разнообразных критериев, позволяющих избавиться от избыточных дизъюнктивных членов. Различные методы, сокращающие поиск доказательства рассматриваются, например, в таких работах, как [Davis ], [Robinson ], [Friedman ]. Наиболее известным и получившим дальнейшее распространение из предлагаемых в этих работах методов является метод резолюций [Robinson ], предложенный Д. А. Робинсоном. Одновременно с методом резолюций и независимо от него С. Ю. Масловым был предложен т. Маслов ]. Последний дает возможность, целенаправленно, опираясь на конкретные особенности доказуемой формулы, ограничить перебор, возникающий при непосредственном применении теоремы Эрбрана и получить вывод более экономным способом, что позволяет экономить вычислительные ресурсы. На данный момент существует целый ряд реализаций программ автоматического поиска доказательств для неклассических логик, основанных, как правило, на методе резолюций или его модификациях. Они описаны в следующих статьях: [Giuchinglia et al. Giunchinglia et al. Hustadt and Shmidt ], [Weidenbach et al. Horrocks and Patel-Schneider ] и [Horrocks ]. Наболее эффективная программа автоматического поиска доказательства, основанная на обратном методе - система К-обратное К - реализована лишь недавно А. Воронковым [Voronkov ]. В работе [Voronkov ] подробно описывается алгоритм автоматического поиска доказательства, основанный на формулировке обратного метода в терминах исчисления путей, и исследуется несколько критериев избыточности, которые позволяют заметно сократить пространство поиска вывода. К-обратное К может вполне успешно конкурировать с программами автоматического поиска доказательства, основанными на методе резолюций, семантических таблиц и/или различных их модификациях. Помимо этого существует несколько работ, посвященных реализации обратного метода для таких неклассических логик, как S4, линейной и интуиционистской логики ([Mints ], [Tammet ], [Tammct ] и [Mints at al. В [Voronkov ] приведена общая схема обратного метода для неклассических логик. До сих пор не была рассмотрена такая важная неклассическая система, как КТ или логика знания. В ней модальный оператор D принимает значение “известно”. Такая трактовка оператора С позволяет говорить о широком спектре применимости экспертных систем, логической моделью машины вывода которых являє гея логика КТ. В связи с вышеизложенным возникает актуальная проблема реализации разрешающей процедуры, основанной на обратном методе для логики знаний. В случае удачного разрешения этой проблемы мы можем получить теоретическое обоснование построения машины вывода для управления базой знаний, формализуемой логической системой КТ. Как уже отмечалось, в настоящее время существует ряд программ автоматического поиска доказательства, в основе большинства из которых лежат традиционные методы резолюций, семантических таблиц, а также различные их модификации. Лучшие из этих систем, такие как *SAT или DLP, ориентированы на тот или иной класс формул; они постоянно улучшаются путем добавления различных стратегий и эвристик, что позволяет говорил, об их практической применимости. К [Voronkov ]. Сформулируем описанную выше проблему более подробно. Пусть Ф - некоторая формула модальной логики КТ. Основной задачей, которую призвана решить эта работа, является получение ответа на вопрос: «Выводима ли Ф в КТ, т. КТSeq? Поскольку для поиска вывода формулы Ф был избран обратный метод установления выводимости, то решение сформулированной проблемы, сводиться к целому ряду подзадач, перечисленных ниже. Построение алгоритма установления выводимости для произвольной формулы модальной логики знания. Построение базовых исчислений обратного метода для логики знания -исходного секвенциального исчисление KTSeq и обратного исчисления секвенций для поиска доказательства конкретной модальной формулы Ф. Мы обозначаем его КТ (ПУ. Доказательство теоремы полноты для исчисления КТф|т.