Разработка и реализация алгоритма поиска вывода в расширении бесконечнозначной предикатной логики Лукасевича

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

Оглавление

1. Введение и предварительные сведения

1.1. Актуальность решаемых задач и обзор близких работ

1.1.1. Бесконечнозначная предикатная логика Лукасевича .

1.1.2. Усиление выразительности логики Лукасевича

1.1.3. Разработка методов и средств для автоматического

доказательства в логике Лукасевича.

1.1.4. Реализация эффективного алгоритма решения систем

линейных двучленных неравенств.

1.2. Цели рабоь

1.3. Краткое содержание работы

2. Расширение бесконечнозначной предикатной логики Лукасевича
2.1. Язык логики и его семантика
2.1.1. Язык логики.
2.1.2. Семантика.
2.1.3. Соотношение с логикой Лукасевича
2.2. Секвенциальное исчисление
2.2.1. Правила вывода
2.2.2. Аксиомы.
2.3. Некоюрые свойства исчисления.
2.3.1. Семантическое обоснование исчисления
2.3.2. Непротиворечивость исчисления.
2.3.3. Связь с исчислением для классической двузначной логики .
2.3.4. Вопросы полноты и разрешимости исчисления
2.3.5. Минуснормализация вывода
2.4. Подлогика двучленных нечетких неравенств
3. Алгоритм поиска вывода
3.1. Идея алгоритма и основные определения.
3.2. Описание шагов алгоритма
3.2.1. Алгоритм Ixi.
3.2.2. Алгоритм i.
3.2.3. Требования к алгоритму i. 7
3.2.4. Главный алгоритм v.
3.2.5. Пример поиска вывода.
3.3. О корректности алгоритма
3.3.1. Свойства алгоритма Ixi.
3.3.2. Свойства алгоритма i.
3.3.3. Свойства главного алгоритма v
3.3.4. Выбор алгоритма i
4. Программная реализация алгоритма поиска вывода
4.1. Общая структура.
4.1.1. Пакет v.
4.1.2. Пакет v.
4.1.3. Пакет v..
4.1.4. Пакет v..x.
4.2. Представление формул и секвенций
4.3. Сишакеический анализатор
4.4. Дснлизация алгоритма поиска вывода.
4.4.1. Заготовка вывода.
4.4.2. Тактики поиска вывода.
4.4.3. Контрприменение правила вывода.
4.4.4. Унификация и распознавание аксиом.
4.5. Предоставляемый программный интерфейс
4.5.1. Создание формул и секвенций
4.5.2. Поиск вывода секвенции
4.5.3. Получение информации о ходе поиска вывода
5. Алгоритм решения систем линейных двучленных неравенств и его программная реализация
5.1. Алгоритм проверки совместноеи систем.
5.1.1. Поыановка задачи и основные определения.
5.1.2. Метод исключений переменных
5.1.3. Алгоритм добавления ограничения в систему
5.1.4. Главный алгоритм проверки совместности систем . .
5.2. Оценка временной сложности алгоритма проверки совместности систем
5.2.1. Вычисли 1ельная модель
5.2.2. Представление системы в памяти
5.2.3. Оценка временной сложности.
5.3. Алгоритм решения сисхем
5.4. Программная реализация алгоритма решения систем
5.4.1. Общая сфуктура
5.4.2 Декомпозиция алгоритмов.
5.4.3. Предоставляемый программный интерфейс.
5.4.4. Экспериментальные результаты .
6. Заключение
Литература


Теорема 1. Для бескопечнозначной предикатной логики Лукасевича не существует удовлетворяющее требованию (DAR), семантически обоснованное и полное исчисление. Д о к а з а т е л ь с т в о. Если бы существовало такое исчисление, то можно было бы построить алгоритм Е, которому подается на вход формула ф. Алгоритм Е последовательно перебирает всевозможные конечные списки слов, проверяет с помощью алгоритма D, является ли очередной список выводом формулі»! Существование упомянутого алгоритма D, очевидно, обеспечивается разрешимостью множества аксиом исчисления и множества пар, задаваемых применениями правил вывода. Таким образом, алгоритм Е выдает ответ «общезначима», если и только если входная формула общезначима, что противоречит неперечислимости множества общезначимых формул бесконечнозначной предикатной логики Лукасевича. Известные исчисления гильбертовского типа для бесконсчпозначиой предикатной логики Лукасевича неполны по указанной причине. Но все же исчисления для этой логики могут служить инструментами для получения многих общезначимых формул. По-видимому, такая ситуация напоминает ситуацию, связанную с неполнотой арифметики Пеано: общезначимая, но не выводимая в арифметике формула обычно искусственна, а задача изобретения такой естественной формулы очень трудна (см. Таким образом, неполнота исчислений для бесконечнозначной предикатной логики Лукасевича не являвши препятствием для исследований и применений различных исчислений (см. И'1ак, разрабохка удобных для поиска вывода исчислений для бесконечнозначной предикатной логики Лукасевича и реализация компьютерных программ для поиска вывода является перспективной исследовательской задачей. Задача распознавания аксиомы секвенциального исчисления, предложенного в данной рабою, сводится к проверке несовместности системы строгих и нестрогих линейных неравенств с целочисленными коэффициентами и рациональнозначиыми переменными. Особая роль систем линейных двучленных неравенств будет показана ниже в контексте вводимой логики и исчисления (см. Здесь же осветим общий контекст, в котором эффективный алгоритм решения систем линейных двучленных неравенств занимает важное месю среди алгоритмов линейного программирования для решения систем линейных неравенств и является практически полезным. Под алгоритмом решения сисюмы понимаеюя алгоритм, который либо выдает одно из решений системы, либо сообщает’ о несовместности системы. Рассмофим задачу определения совместности (или решения) системы из т нестрогих линейных неравенств с целочисленными коэффициентами относительно п рациональнозначных переменных. Хорошо известно (см. Для решения рассматриваемой задачи можно применить полиномиальные алгоритмы Л. Г. Хачияна [] или Н. Кармаркара []. Число выполняемых этими алгоритмами арифметических операций зависит от величины коэффициентов СИС1СМЫ. Определение 1. Алгоритм называется сильно полиномиальным, если он полиномиален (но числу шагов при реализации на машине Тьюринга), и число элемешариых арифметических операций (сложение, вычитание, умножение, деление, сравнение), выполняемых им над рациональными числами, ограничено полиномом от числа целых чисел на входе ([], [, с. Таким образом, число элементарных арифметических операций, выполняемых сильно полиномиальным алгоритмом, не зависит от величин целых чисел на входе. Замечание 1. Отмстим, что сильно полиномиальный алгоритм также называют истинно полиномиальным алгоритмом (см. Однако в определении истинно полиномиального алгоритма из [, с. Па наш взгляд, это существенное требование, выражающее, в частности, ограничение на возможную неэффективность организации сіруктур данных, используемых в алгоритме. До сих пор остается открытым вопрос о существовании сильно полиномиального алгоритма для определения совместности сисіем общею вида. Однако известны сильно полиномиальные алгоритмы для решения систем линейных неравенств с не более чем двумя переменными в каждом неравенстве, причем допускаются только нестрогие неравенства [, , ], На настоящий момент* (ср.