Диссертация (Автоматический логический вывод в интуиционистских логических исчислениях обратным методом Маслова), страница 4

В настоящей работе оба термина рассматриваются каксинонимы.17которого является либо аксиомой, либо одной из формул, либо следствиемкаких-либо предыдущих формул по одному из правил вывода исчисления L.Доказательство произвольной формулы F также можно представить в видедерева вывода (дерева доказательства), где в вершинах находятся формулы, аребрам соответствуют применения правил. Деревья вывода принято изображатьтак, что посылки правил находятся над их заключениями. При этом в корнедерева находится формула F, а его листьями являются аксиомы.Высотой вывода (дерева вывода) называется число формул в его самойдлинной ветви, а длиной вывода — общее число вхождений формул в вывод.Сложностью вывода называется число формул в его линейной записи(не содержащей повторяющихся формул).Выделяют два направления поиска вывода: сверху вниз (от аксиом кдоказываемой формуле) и снизу вверх (от доказываемой формулы к аксиомам).При поиске вывода снизу вверх по виду конечной формулы восстанавливаетсявид применений правил вывода (или аксиом), заключением которых можетявляться эта формула, затем та же процедура повторно применяется к посылкамэтих применений и так далее.Список формул, доказанных на конкретной стадии процесса поиска вывода,называется пространством поиска вывода, а его представление в виде дерева —деревом поиска вывода.

Если поиск вывода идет в направлении сверху вниз, тоэто дерево может не иметь выделенного корня.Свойство подформульности логического исчисления выполняется, если ввыводе произвольной формулы могут участвовать только ее подформулы14.Логическое исчислениеназывается разрешимым, если существуеталгоритм, для произвольной заданной формулыопределяющий, выводима ли формулазавершающий работу ив исчисленииназывается разрешающим алгоритмом для исчисления14. Такой алгоритм. Аналогично можетТочное определение понятия подформулы приводится в параграфе 2.2.

Определение свойстваподформульности для секвенциальных исчислений дается там же.18быть определен разрешающий алгоритм для некоторого класса формул из , еслиисчислениев целом не является разрешимым.Алгоритмом поиска вывода для исчисления L называется алгоритм,позволяющий найти вывод произвольной формулы A в исчислении, еслиформула A действительно выводима. Для невыводимых формул такой алгоритмможет не завершить свою работу.Метод поиска вывода (метод АЛВ) — способ автоматизации поискавывода в том или ином логическом исчислении.Стратегия поиска вывода — способ экономной организации процессапоиска вывода в некотором логическом исчислении.

Может заключаться,например, в удалении избыточных ветвей дерева поиска вывода или виспользовании фиксированного порядка применений правил вывода.Стратегия поглощения15 — одна из основных стратегий поиска выводадля разных методов АЛВ, позволяющая исключать из рассмотрения избыточныеветви дерева поиска вывода.Перед применением ряда методов автоматического логического выводанеобходимо приводить формулы к некоторому стандартизованному виду,упрощающему процесс поиска доказательств.

Такой стандартизованный способзаписи называется «нормальной формой».Говорят, что формула логики высказываний находится в конъюнктивнойнормальной форме (КНФ), если она имеет вид конъюнкции дизъюнкцийлитералов (литералом называется атомарная формула или ее отрицание).Формула логики первого порядка находится в предваренной нормальнойформе, если она имеет вид(или), а, где— кванторы— формула, не содержащая кванторов.В тексте работы имеются ссылки на библиотеки TPTP и ILTP. Вторая изних использовалась для испытания разработанной программы АЛВ (см. главу 4).15В книге [50] эта стратегия для метода резолюций называется стратегией вычеркивания. В англоязычнойлитературе используется термин «subsumption strategy».19TPTP (название расшифровывается как Thousands of Problems for TheoremProvers) — обширная библиотека задач для тестирования и сравнения программАЛВ (в основном ориентированная на программы АЛВ для классической логикипервого порядка).

Библиотека TPTP версии 6.0.0 содержит 20306 разноплановыхзадач. Подробное описание см. в статье [137] и на сайте [145].ILTP (название расшифровывается как Intuitionistic Logic TheoremProving) — библиотека задач, созданная в целях тестирования и сравненияпрограмм АЛВ для интуиционистской логики по образцу TPTP. Библиотекавключает как математические, так и формализованные технические задачи,которые возникают при верификации программных и аппаратных систем, а такжевразличныхприложенияхискусственногоинтеллекта.Текущаяверсиябиблиотеки ILTP (версия 1.1.2) содержит около 2800 задач: 274 задачи на языкелогики высказываний и 2550 задач на языке логики первого порядка.

Описаниебиблиотеки приведено в статье [121], результаты сравнения программ АЛВ — насайте [144].Формальная верификация — метод верификации (проверки) программногоили аппаратного обеспечения, основанный на формальном доказательствесоответствия проверяемой системы заданным требованиям.1.3. Интуиционизм и конструктивизм: краткая историческая справкаИнтуиционизм — совокупность философских и математических идей,рассматривающихмысленныхматематикупостроениях[9].какнаукуобРодоначальникоминтуитивноубедительныхинтуиционизмасчитаетсяЛ.

Э. Я. Брауэр, который в начале XX века выступил с критикой некоторыхабстракцийипринциповдоказательстваутверждений,используемыхв(классической) математике. Интуиционизм наряду с формализмом Д. Гильбертастал одним из основных направлений выхода из так называемого «кризиса20оснований математики», который проявился на рубеже XIX–XX веков и былсвязан с обнаружением теоретико-множественных парадоксов16.Интуиционисты предъявляют к умственным построениям требованиеинтуитивнойпонятностииубедительности.Поэтомуинтуиционистыотказываются от абстракции актуальной бесконечности, а также от доказательств«чистого» существования, когда существование математического объекта стребуемыми свойствами доказывается без указания способа построения искомогообъекта17.Какправило,висключенного третьеготакихдоказательствахиспользуетсяили закон двойного отрицаниязакон.

Винтуиционизме отвергается универсальная применимость этих классическихзаконов.Основнымиматематическимиобъектамивинтуиционистскойматематике являются натуральные числа, а основным методом доказательства —метод математической индукции.СогласноопределениюА. Г. Драгалина[9, с. 511],интуиционистскаялогика представляет собой совокупность методов доказательства утверждений,приемлемых с точки зрения интуиционизма.

Стандартные логические связки винтуиционистской логике интерпретируются иначе, чем в классической логике.Например, из интуиционистского доказательства утвержденияможно извлечь конкретный примерутверждениявсегдаи доказательство соответствующего. Из интуиционистского доказательства утвержденияможно извлечь информацию, какое из утвержденийиявляется истинным, атакже доказательство указанного утверждения18. Поэтому утверждениеможет не выполняться в интуиционистской логике, еслина данный момент недоказано и не опровергнуто (т.

е. представляет собой нерешенную задачу).16См. обсуждение проблем оснований математики в книге [13].17Примеры таких доказательств содержатся во многих книгах и статьях, посвященных интуиционистскойлогике. Например, в монографии [10] приведен пример доказательства «чистого» существования такихиррациональных чисел a и b, что18рационально.Неформальную интуиционистскую интерпретацию других логических связок см. в [10].21А. Н. Колмогоров в статье 1925 года предложил логическое исчисление врамках ослабленного варианта интуиционистской логики, в котором непринимается принцип «из ложного следует все, что угодно» [17]. РассмотреннаяА.

Н. Колмогоровым логика получила название минимальной логики. В 1928 годудругой советский ученый В. И. Гливенко сформулировал интуиционистскоеисчисление высказываний [75], см. также формулировку в изложении Г. Генцена[5, с. 61–62]. В 1930 году А. Гейтинг, ученик Л. Э. Я. Брауэра, предложил своюформализацию интуиционистской логики [85]. Хоть работы А. Н.

Колмогорова иВ. И. Гливенко и вышли раньше, именно формализация А. Гейтинга получиланаибольшуюизвестность.Формулировкуинтуиционистскогоисчисленияпредикатов Гейтинга (HPC) можно найти в монографии А. Г. Драгалина [10].Гильбертовский вариант исчисления Гейтинга можно также найти в статьеГ. Генцена [5] и в книгах С. К. Клини [13, 14]. Позднее, в 1934 году, Г. Генценпредложил интуиционистское исчисление предикатов LJ (см. русский перевод встатье [5]).Несмотря на то, что Брауэр выступал против формализации своей логики,именно формулировка интуиционистских исчислений позволила точнымиматематическими методами исследовать важные свойства интуиционистскойлогики, при этом философские вопросы отошли на второй план. В 1932 годуА.