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

• Автор: Смирнова, Елена Сергеевна
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2002
• Место защиты: Санкт-Петербург
• Количество страниц: 135 с. : ил

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

ГЛАВА I ВВЕДЕНИЕ В ОБОБЩЕННУЮ ЛОГИКУ ПОСТА.

1.1. Множества логических значений.

1.2. Синтаксис и семантика.

1.2.1. Внутренний уровень.

1.2.2. Внешний уровень

I 3. Секвенциальное исчисление.

1.3.1. Секвенции

1.3.2. Вывод и правила вывода.

1.3.3. Теоремы и аксиомы

ГЛАВА II РАСПОЗНАВАНИЕ АКСИОМ ОБОБЩЕННОЙ ЛОГИКИ ПОСТА.
2.1. Подготовка и преобразование секвенции для тестирования
2.2. Метод установления неразрешимости систем элементарных линейных
неравенств
2.2.1. Постановка задачи
2.2.2. Преобразование системы.
2.2.3. Необходимое и достаточное условие неразрешимости систем элементарных линейных неравенств
2 2 4 Доказательство необходимости условий неразрешнмости.
2.2.5. Представление системы в виде графа.
2.2.6. Доказательство достаточности условий неразрешимости
2.3. Алгоритм проверки разрешимости системы элементарных линейных
неравенств
2.4. Сложносгь атгоритма проверки разрешимости системы элементарных
линейных неравенств.
2.5 Случай множества логических значений, несимметричного относительно
2.5.1. Доказательство взаимооднозначносги преобразования множес тва значений
2.5.2. Доказательство сохранения несов.честности преобразованной системы
2.5.3. Примеры преобразований несимметричного множества значений системы неравенств.
2.6 Алгоритм распознавания аксиом обобщенной логики Поста.
ГЛАВА III. ОПИСАНИЕ АЛГОРИТМА ПОИСКА ВЫВОДА.
3.1. редставление вывода.
3.2. Представление формул и секвенций .
3.2.1. Представление формул.
3.2.2. Представление секвенций
3 3. Поиск правил и порядок их применения
3 3.1 Выбор главного члена секвенции
3.3.2. Поиск применимых правил
3.3.3. Значение порядка применения правил.
3.3.4.Таблицы приоритетов выбора правил.
3.4 Кванторные правила и их ограничения.
3.4 1 Раскрытие кванторов и унификация
3.4.2. Ограничения на подстановку. Параметры в кванторных правилах
3.4.3. Усиление ограничений в кванторных правилах
3.4 4. Домены для подстановки
3.4.5. Стратегия замораживания повторяющихся кванторных формул и
ограничения на число их раскрытий.
3.5. Схема алгоритма вывода.
3.6. Дополнительные опции вывода
3.6.1. Выявление расширенных аксиом
3.6.2. Стратегии проверки элементарных секвенций.
3.6.3. Установка параметров унификации.
3.7 Параметры алгоритма выявления аксиом.
ГЛАВА IV. ОПИСАНИЕ СИСТЕМЫ .АВТОМАТИЧЕСКОГО ПОИСКА ВЫВОДА
4.1. Структура данных и реализация алгоритма
4.1.1. Структура программы.
4.1.2. Представление данных
4 1.3. Реализация основных частей атгоритма
4.2. Общий вид и назначение системы.
4.3. Подготовка входных данных
4.3.1. Настройка параметров лог ики
4.3.2. Ввод исследу емой формулы
4.4 Установка дополнительных параметров системы автоматического
построения вывода.
4.4.1. Выбор стратегий
4.4.2. Дополнительные настройки системы.
4.5 Задание имен входных и выходных файлов
4.6. Запуск и работа основного алгоритма.
4.6.1. Автоматический режим вывода
4.6.2. Интерактивный режим вывода.
4.7. Представление и просмотр результатов работы алгоритма.
ЗАКЛЮЧЕНИЕ
ЛИТЕРАТУРА


В [ показано, что различная последовательность примененных правил может в значительной степени отражаться на длине и ширине дерева вывода, и предложена стратегия выбора правил в зависимости от вида обрабатываемых секвенций В ходе апробации программы было проведено свыше 0 тестовых выводов, охватывающих возможные виды секвенций В результате этого была создана база данных системы, на основании которой созданный алгоритм выбирает правило в создавшейся ситуации. В главе 4 описаны структуры данных и основные процедуры реализации атгоритма, приведены фрагменты программною кода с объяснениями. Также отражены основные возможностей системы, описан ее интерфейс и предлагаемых в ней сервисы, среди которых можно перечислить как автоматический, так и “ручной” вывод исходной секвенции, проверку разрешимости систем элементарных линейных неравенств, возможность работы в многооконном текстовом редакторе, использование системы подсказок и прочее Общее описание интерфейса системы приведено в [4]. Затача системы автоматического построения вывода заключается в генерации последовательности примененных правил, получении списка элементарных секвенций и в проверке каждой из них на аксиоматичность. Основными входными данными программы являются формула, вывод которой должен быть построен, и параметры логики, в которой этот вывод будет производиться. Алгоритм проверки выводимости секвенции состоит из двух основных частей: процедуры построения вывода и процедуры проверки полученных элементарных секвенций на предмет выявления аксиом. Предусмотрена возможность использования этих частей алгоритма независимо друт от друга: например если уже имеется список элементарных секвенций, то их можно отдельно исследовать на аксиоматичность. Одна из основных задач алгоритма поиска вывода состоит в выборе на каждом шаге правила, позволяющего получить наименьшее дерево вывода (сократить длину вывода) Интересен тот факт, что если в классической логике для получения минимазьного дерева вывода всегда, по возможности, избегают ветвления секвенции, предпочитая увеличивать глубину дерева ради сокращения его ширины, то в обобщенной логике Поста это далеко не всегда так Например, если при выводе формулы —» ( ~'(C/D) < (Л&В)). Если же двухпосылочное правило использовать в самом начале, то для вывода этой формулы понадобиться 5 применений правил, а элементарных секвенций получится всего две. Таким образом, перед системой автоматического поиска вывода, встает задача подбора правил, дающих наиболее короткий вывод. Система создана с использованием языка Delphi версии 4. DOS и Unix реализована с помощью Visual Prolog версии 4. Объем предоставленной реализации составляет приблизительн строк на языке Delphi. Объем объектного кода - примерно 0 КБ. Среди основных результатов данной диссертационной работы можно отметить разработку оптимизирующей стратегии поиска вывода секвенций в обобщенной логике Поста, теоретическую доработку и реализацию алгоритма проверки разрешимости систем линейных неравенств специального вида, разработку и реализацию основного алгоритма построения вывода в обобщенной логике Поста и создание интегрированной интерактивной системы на основании этого алгоритма опубликованных в [1], [4], [5] и (]. Глава I. В качестве множества логических значений предикатов и констант, принадлежащих внутреннему уровню обобщенной логики Поста, предложено рассматривать целые или рациональные числа из фиксированного промежутка на числовой прямой. Выделяются два варианта первый, при котором множество логических значений симметрично относительно нуля (возможно не включая сам ноль) и второй, когда промежуток произволен Во втором случае как правило рассматривают отрезок [0, 1 ]. Рассмотрим первый вариант, при котором логические значения выбираются из симметричного относительно нуля множества Лг = -к, к] или = [-? О, где к -некоторое фиксированное для данной лотки натуральное число. В общем случае множеством логических значений является множество Ьг - а, Ь о 1 или ? Ь - произвольные целые числа. Более подробно особенности этого случая будут рассмотрены в главе 2. Как было отмечено, предикаты и логические константы внешнего уровня принимают значения из двухэлементного множества {ЛОЖЬ, ИСТИНА}.