ОГЛАВЛЕНИЕ
ВВЕДЕНИЕ.
ГЛАВА 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. Представление и просмотр результатов работы алгоритма.
ЗАКЛЮЧЕНИЕ
ЛИТЕРАТУРА
- Київ+380960830922