Диссертация (Автоматический логический вывод в интуиционистских логических исчислениях обратным методом Маслова)
Описание файла
Файл "Диссертация" внутри архива находится в папке "Автоматический логический вывод в интуиционистских логических исчислениях обратным методом Маслова". PDF-файл из архива "Автоматический логический вывод в интуиционистских логических исчислениях обратным методом Маслова", который расположен в категории "". Всё это находится в предмете "физико-математические науки" из Аспирантура и докторантура, которые можно найти в файловом архиве СПбГУ. Не смотря на прямую связь этого архива с СПбГУ, его также можно найти и в других разделах. , а ещё этот архив представляет собой кандидатскую диссертацию, поэтому ещё представлен в разделе всех диссертаций на соискание учёной степени кандидата физико-математических наук.
Просмотр PDF-файла онлайн
Текст из PDF
САНКТ-ПЕТЕРБУРГСКИЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ ПЕТРА ВЕЛИКОГОНа правах рукописиПавлов Владимир АлександровичАвтоматический логический вывод в интуиционистскихлогических исчислениях обратным методом МасловаСпециальность 05.13.11 —«Математическое и программное обеспечение вычислительных машин,комплексов и компьютерных сетей»Диссертация на соискание ученой степеникандидата физико-математических наукНаучный руководителькандидат технических наук, доцентЩукин Александр ВалентиновичСанкт-Петербург20172ОГЛАВЛЕНИЕВВЕДЕНИЕ ......................................................................................................................
4ГЛАВА 1. ОБЗОР ПРЕДМЕТНОЙ ОБЛАСТИ .......................................................... 131.1. Введение ........................................................................................................... 131.2. Основные определения и обозначения .......................................................... 131.3. Интуиционизм и конструктивизм: краткая историческая справка ............ 191.4. Программыавтоматическогологическоговыводаиобластиихприменения ..............................................................................................................
231.5. Методы поиска вывода для логики первого порядка .................................. 301.6. Заключение ....................................................................................................... 43ГЛАВА 2. ПОСТРОЕНИЕИНТУИЦИОНИСТСКОГОИСЧИСЛЕНИЯОБРАТНОГО МЕТОДА ............................................................................................... 452.1. Введение ........................................................................................................... 452.2. Основные определения и обозначения .......................................................... 462.3. Универсальная методика построения логических исчислений, подходящихдля применения обратного метода ........................................................................ 562.4.
Пример односукцедентного исчисления обратного метода ........................ 572.5. Построение многосукцедентного исчисления обратного метода............... 602.6. Особенности построенного многосукцедентного исчисления ................... 752.7. Пример ..............................................................................................................
762.8. Модификации исчислений .............................................................................. 802.9. Заключение ....................................................................................................... 81ГЛАВА 3. РАЗРАБОТКАСТРАТЕГИЙПОИСКАВЫВОДАДЛЯИНТУИЦИОНИСТСКИХ ИСЧИСЛЕНИЙ ОБРАТНОГО МЕТОДА ..................... 833.1. Введение ........................................................................................................... 833.2. Основные определения и обозначения .......................................................... 843.3.
Стратегия поглощения секвенций.................................................................. 843.4. Стратегия упрощения секвенций ................................................................... 883.5. Стратегии удаления недопустимых секвенций ............................................
9333.6. Стратегия тривиального сокращения ............................................................ 993.7. Сингулярная стратегия .................................................................................... 993.8. Совместимость стратегий ............................................................................. 1003.9. Применение стратегий к модификациям исчислений ............................... 1023.10.
Примеры........................................................................................................ 1033.11. Заключение ................................................................................................... 110ГЛАВА 4. АЛГОРИТМ ПОИСКА ВЫВОДА И ПРОГРАММНАЯ РЕАЛИЗАЦИЯОБРАТНОГО МЕТОДА ............................................................................................. 1124.1. Введение ......................................................................................................... 1124.2. Основные определения и обозначения ........................................................
1124.3. Алгоритм поиска вывода............................................................................... 1134.4. Программа для автоматического поиска вывода WhaleProver ................. 1174.5. Результаты экспериментов на задачах из библиотеки ILTP ..................... 1204.6. Сравнение программы WhaleProver с существующими программами АЛВдля интуиционистской логики первого порядка ............................................... 1284.7. Интерактивный режим ..................................................................................
1334.8. Заключение ..................................................................................................... 138ЗАКЛЮЧЕНИЕ ........................................................................................................... 141СПИСОК СОКРАЩЕНИЙ И УСЛОВНЫХ ОБОЗНАЧЕНИЙ .............................. 143СПИСОК ИСПОЛЬЗОВАННОЙ ЛИТЕРАТУРЫ ................................................... 144ПРИЛОЖЕНИЕ А. ДОКАЗАТЕЛЬСТВА ПРОМЕЖУТОЧНЫХ УТВЕРЖДЕНИЙИЗ ГЛАВЫ 2 ................................................................................................................
160ПРИЛОЖЕНИЕ Б. ДОКАЗАТЕЛЬСТВА ПРОМЕЖУТОЧНЫХ УТВЕРЖДЕНИЙИЗ ГЛАВЫ 3 ................................................................................................................ 182ПРИЛОЖЕНИЕ В. ЗАДАЧИ ИЗ БИБЛИОТЕКИ ILTP, ИСПОЛЬЗОВАННЫЕПРИ СРАВНЕНИИ СТРАТЕГИЙ ПОИСКА ВЫВОДА ......................................... 198ПРИЛОЖЕНИЕ Г. РЕЗУЛЬТАТЫТЕСТИРОВАНИЯПРОГРАММЫНАЗАДАЧАХ ИЗ БИБЛИОТЕКИ ILTP .........................................................................
2034ВВЕДЕНИЕАктуальность темы исследованияДиссертационнаяС. Ю. Масловадляработапосвященаавтоматизацииприменениюпоискаобратногологическогометодавыводавинтуиционистской логике первого порядка.Вопросы автоматизации доказательств изучаются в ведущих научноисследовательских институтах мира.
Данная область исследований на стыкематематическойлогикииискусственногоинтеллектаназываетсяавтоматическим логическим выводом (АЛВ)1. Программные средства дляавтоматического поиска логического вывода, называемые программами АЛВ(«пруверами»)2, активно применяются в математике, в системах искусственногоинтеллекта, а также при решении задач формальной верификации и синтеза ПО3.Интуиционистскиелогическиеисчисленияширокоиспользуютсявматематической логике и в различных разделах информатики.
Одной из наиболеевостребованных особенностей этих исчислений является возможность издоказательствасуществованиянекоторогообъектаизвлечьспособегопостроения. В настоящей работе под интуиционистской логикой первогопорядка понимается исчисление предикатов А. Гейтинга [85] (см. также [10]) иравнообъемные ему исчисления. В отличие от классического исчисленияпредикатов, в интуиционистском исчислении невыводимы классические законыисключенного третьегои снятия двойного отрицания.Программы АЛВ для интуиционистской логики первого порядка находятприменение в интерактивных программах АЛВ (для логик высшего порядка),1Термин «автоматическое доказательство теорем» (АДТ) в работе используется как синоним АЛВ.2Термин «прувер» (от англ.
prover — средство доказательства) часто употребляется в техническойлитературе по АДТ. Ввиду специфичности термина мы его употребляем в кавычках. Также распространенытермины «система автоматического доказательства теорем», «система поиска вывода». В настоящей работе от ихиспользования было решено отказаться, так как в русском языке, особенно в научной среде, слово «система» необязательно ассоциируется с единичным программным продуктом.3Программное обеспечение.5таких как Coq и Nuprl [127, 65], где они используются в качестве тактик поискавывода и позволяют частично автоматизировать решение сложных задач.
Однакоэксперименты показывают, что эти тактики пока обладают недостаточно высокойрезультативностью (см. [96] и [144]). Поэтому поставленная задача важна дляповышения степени автоматизации интерактивных программ АЛВ, в том числепри их использовании для верификации и синтеза ПО.Степень разработанности темыСреди методов логического вывода для классической логики первогопорядка наибольшее распространение и развитие получил метод резолюций [123],позволяющий устанавливать выводимость формул, приведенных к сколемовскойстандартной форме (см.
книгу [50]). Однако к интуиционистской логике методрезолюций неприменим, так как в ней не все формулы могут быть приведены куказанному виду эквивалентными преобразованиями.В программах АЛВ для интуиционистской логики обычно используютсятабличныеметодылогическоговывода[1, 79].Однакосуществующиепрограммные реализации пока не справляются с достаточно сложными задачами,что подтверждается опубликованными в сети Интернет результатами ихтестирования на библиотеке ILTP [144].
