Диссертация (1149226), страница 3
Текст из файла (страница 3)
Доказывается12равнообъемность этого исчисления и исчисления GHPC А. Г. Драгалина [10].Приводится пример вывода формулы в построенном исчислении.В главе 3 рассматриваются стратегии поиска вывода для предложенногоисчисления,применимыетакжексуществующиминтуиционистскимисчислениям обратного метода, например к исчислениюиз работы [68].Доказывается полнота каждой стратегии и любой их комбинации.
Приводятсяпримеры вывода формул, демонстрирующие работу стратегий.В главе 4 формулируется алгоритм поиска вывода обратным методом,позволяющий комбинировать стратегии поиска вывода и применимый кразличным исчислениям обратного метода. Дается описание разработаннойпрограммы АЛВ WhaleProver, в которой используется рассмотренный алгоритм.Приводятся результаты экспериментов с программой WhaleProver на задачах избиблиотеки ILTP: сравнение стратегий поиска вывода, сравнение программы ссуществующими аналогами.Каждаяглаваначинаетсясобственнымвведениемизавершаетсязаключением. Во втором параграфе каждой главы приводятся основныеопределения и обозначения, используемые в той главе и во всех последующихглавах (чтобы облегчить чтение работы, новые определения вводятся по меренеобходимости в начале каждой главы).
В работе используется стандартный языклогики первого порядка (см. параграф 1.2). Нумерация теорем, лемм, замечаний исоглашений, формул, рисунков и таблиц идет в пределах каждой главы.Нумерация примечаний сквозная по всему документу. Доказательства теорем илемм начинаются символоми заканчиваются символом. Для упрощениявосприятия текста некоторые объемные доказательства вынесены в приложения.13ГЛАВА 1. ОБЗОР ПРЕДМЕТНОЙ ОБЛАСТИ1.1. ВведениеНастоящая глава посвящена обзору предметной области. В параграфе 1.2приводятся основные определения и обозначения, используемые в этой главе и вовсехпоследующих.Впараграфе1.3краткорассматриваетсяисторияинтуиционизма и особенности интуиционистских (конструктивных) теорий. Впараграфе 1.4 приводится обзор программ АЛВ и областей их применения. Впараграфе 1.5 рассматриваются основные методы АЛВ для логики первогопорядка: метод резолюций, табличные методы и обратный метод.
Приводитсяподробный обзор литературы по обратному методу. В параграфе 1.6 подводятсяитоги главы.Основные результаты обзора, содержащегося в этой главе, изложены впубликациях автора [114, 116, 115, 44].1.2. Основные определения и обозначенияБольшую часть данных ниже определений можно найти в учебниках поматематической логике и теории доказательств [14, 32, 50].Определения автоматического логического вывода (АЛВ), программ АЛВ(«пруверов») и интуиционистской логики первого порядка были приведены вовведениикдиссертационнойработе.Понятияинтуиционистскойиконструктивной логики в работе рассматриваются как синонимы и понимаются внаиболее широком смысле8.Логика высказываний изучает связи между высказываниями, которыестроятся8путемсоединенияатомарныхвысказыванийспомощьюКонструктивное направление в математике разрабатывалось научной школой А.
А. Маркова. СамА. А. Марков подчеркивал отличия своей концепции от интуиционизма (см. его комментарии к русскоязычномуизданию книги [4]). Однако в настоящее время термины «интуиционистский» и «конструктивный» применительнок логическим исчислениям обычно используются как синонимы (называть интуиционистское исчислениеконструктивным предложил А.
Н. Колмогоров). Данный вопрос также затрагивается в параграфе 1.3.14пропозициональных связок. Атомарные высказывания представляют собойповествовательные предложения, которые могут быть истинными или ложными(их внутренняя структура не анализируется). Примеры высказываний: «Мелбелый», «Волк — хищник», «Андрей Аршавин играет за Зенит».Логикапервогопорядка(логикапредикатов)расширяетлогикувысказываний возможностью анализа внутренней структуры высказываний.
Дляэтого вводятся новые операции, называемые кванторами, а также термы(предметные переменные, предметные константы и функции) и предикаты(функции относительно термов, значениями которых являются высказывания).В работе используется стандартный язык логики первого порядка, сиспользованием следующих символов: пропозициональные(конъюнкция),связки(отрицание),(эквивалентность)9;(импликация), символы квантора всеобщности логические константы(дизъюнкция),и квантора существования ;(«истина») и(«ложь»); символы предикатных переменных P, Q, R и т. д.; символы предметных констант c, d; символы предметных переменных x, y, z и т. д.; функциональные символы f, g, h; символы для обозначения произвольных термов r, s, t; символы для произвольных формул A, B, C, D, F, G, ,и т. д.Все символы, за исключением логических операций (пропозициональныхсвязок и кванторов) и логических констант, могут быть пронумерованыподстрочными, надстрочными индексами и (или) дополнены штрихами.Стандартным образом определяемые формулы описанного языка10 будемназывать формулами логики первого порядка.
Аналогично для формул логикивысказываний.9В разных публикациях конъюнкция также может обозначаться символом «&», импликация — символом« », а эквивалентность — символом «~» или «» (см. [14]).15В работе используется следующее соглашение, позволяющее опускатьлишние скобки в выражениях. Во-первых, внешние скобки формулы, как правило,опускаются. Во-вторых, приоритеты логических операций по убыванию «ранга»распределяются так:,,,,,.
При этом связки с более высоким,«рангом» имеют большую область действия. Если две связки имеют одинаковыйранг, то более широкую область действия имеет та, которая находится правее.Например, скобки в формулевосстанавливаются следующим образом:.Таким образом, при наших соглашенияхявляется краткой записью формулы.Логика первого порядка с равенством получается из логики первогопорядка введением предиката равенства.Логика второго порядка расширяет логику первого порядка возможностьювведения кванторов над предикатами. Логики высших порядков получаются излогики второго порядка дальнейшим обобщением.Теория типов, как правило, является расширением логики высшегопорядка, в которой переменные и функции классифицируются с помощьюиерархической структуры типов.
Пример часто используемой теории типов — этолямбда-исчисление с типами.В рамках той или иной логики можно сформулировать разные логическиеисчисления (см. определение ниже), отличающиеся своими свойствами. При этом,как отмечается в [9], не существует такого интуиционистского исчисления,котороебыло(конструктивной)быприемлемологики.Ввоработевсехмывариантахинтуиционистскойограничимсярассмотрениеминтуиционистских исчислений, равнообъемных интуиционистскому исчислениюпредикатов А. Гейтинга [85].10Например, см.
[32, с. 54] или [14, с. 100].16Логическое исчисление (формальная аксиоматическая теория) считаетсяопределенным, если выполняются следующие условия11:1. Задан логико-математический язык, включающий счетное множествосимволов и слов (слово — это конечная последовательность символов).2. Определены правила образования формул из символов и слов.3. Выделено подмножество формул, называемых аксиомами исчисления12.4. Задано конечное множество отношений между формулами, называемыхправилами вывода.Пусть L — логическое исчисление. Если R — правило вывода исчисления Lи формулынаходятся в отношении R с формулой B, то B называетсянепосредственным следствием этих формул по правилу R.
В этом выводе поправилу R формулыназываются посылками, а формула B —заключением.Конечный список формул, каждая из которых является либо аксиомой L,либо непосредственным следствием каких-либо предыдущих формул по одномуиз правил вывода исчисления L, называется (логическим) выводом, илидоказательством в исчислении L13. Если существует доказательство висчислении L, оканчивающееся формулой F, то будем говорить, что F выводима(доказуема) в исчислении L, или что F является теоремой L.Выводом формулы F из гипотезв исчислении L называетсяконечный список формул, оканчивающийся формулой F, всякая формула11Все нижесказанное применимо и к секвенциальным исчислениям (которые являются разновидностьюлогических исчислений), если заменить слово «формула» словом «секвенция».
Секвенциальные исчисленияподробнее обсуждаются в пункте 2.2.4.12В настоящей работе рассматриваются только такие исчисления, в которых по каждой формуле можноэффективным образом определить, является ли эта формула аксиомой исчисления или нет. Для правил выводадействует аналогичное требование эффективности.13В книге [14] термины «вывод» и «доказательство» отличаются по смыслу: первый терминупотребляется, когда речь идет о выводе формулы из некоторых гипотез, а второй — когда в доказательстве неиспользуются никакие дополнительные гипотезы.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
