Диссертация (1149226)
Текст из файла
САНКТ-ПЕТЕРБУРГСКИЙ ПОЛИТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ ПЕТРА ВЕЛИКОГОНа правах рукописиПавлов Владимир АлександровичАвтоматический логический вывод в интуиционистскихлогических исчислениях обратным методом МасловаСпециальность 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].
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
