Некоторые алгоритмические вопросы для формальных систем со свойством интернализации выводов тема диссертации и автореферата по ВАК РФ 01.01.06, кандидат физико-математических наук Крупский, Николай Владимирович

  • Крупский, Николай Владимирович
  • кандидат физико-математических науккандидат физико-математических наук
  • 2006, Москва
  • Специальность ВАК РФ01.01.06
  • Количество страниц 81
Крупский, Николай Владимирович. Некоторые алгоритмические вопросы для формальных систем со свойством интернализации выводов: дис. кандидат физико-математических наук: 01.01.06 - Математическая логика, алгебра и теория чисел. Москва. 2006. 81 с.

Оглавление диссертации кандидат физико-математических наук Крупский, Николай Владимирович

0.1 Введение.

1 Отраженная логика доказательств.

1.1 Основные определения.

1.2 Конструкция наименьшей модели

1.3 Отраженный фрагмент логики доказательств.

1.4 Сложность фрагментов логики доказательств.

2 Типизация термов в рефлексивной комбинаторной логике.

2.1 Определение правильно построенных формул RCL—.

2.2 Типизация подтермов.

2.3 Типы в RCU.

2.4 Соответствие между правильно построенными формулами и типами.

2.5 Восстановление типов.

3 Выводимость в рефлексивной комбинаторной логике.

3.1 Выводимость из гипотез в RCL-*.

3.2 Устранение сечения в RCLTg.

3.3 Разрешимость RCLTg.

3.4 Оценки сложности.

Рекомендованный список диссертаций по специальности «Математическая логика, алгебра и теория чисел», 01.01.06 шифр ВАК

Введение диссертации (часть автореферата) на тему «Некоторые алгоритмические вопросы для формальных систем со свойством интернализации выводов»

Под свойством интернализации выводов для формальной системы Т ниже понимается ее способность формализовать рассуждения про свои собственные выводы и их связь с выводимыми ими формулами. Типичным примером формализма такого рода является формальная арифметика первого порядка РА (арифметика Пеано). Гёделевская нумерация синтаксиса РА (см. [15], [11]) позволяет определить инъек-тивное кодирование формул и выводов натуральными числами таким образом, что предикат доказательств их есть код вывода формулы с гёделевским номером у" оказывается выразимым арифметической формулой Prf(x,y). При этом для любой арифметической формулы ip справедливо

PA b tp PA b Pr/(n, rip~l) для некоторого натурального числа п.

Здесь п — нумерал, соответствующий числу п, а г(р~] — гёделевский номер формулы ip.)

Множество всех теорем РА вида Prf(n,rip~]) образует отраженный фрагмент РА. Фактически, он уже содержит формулировки всех доказуемых в РА утверждений, но в несколько иной форме и с дополнительной информацией про их выводы. В то же время он существенно проще множества всех теорем РА. Естественный выбор деталей кодирования приводит к выражению предиката доказательств посредством Ai-формулы. Это обеспечивает разрешимость отраженного фрагмента, в то время как множество всех теорем РА неразрешимо.

Аналогичное наблюдение имеет место для всех рекурсивно аксиоматизируемых расширений Т теории РА истинными (в стандартной модели арифметики) формулами. Факт разрешимости отраженного фрагмента теории Т является следствием разрешимости отношения d сеть вывод формулы </?" для теории Т, а сама теория Т неразрешима ввиду существенной неразрешимости РА (см. [15]). Поэтому отраженный фрагмент устроен проще всей теории Т. Заметим, что это рассуждение использует факт неразрешимости теории Т и неприменимо в случае разрешимых теорий. Для ряда разрешимых формализмов вопрос о сравнении проблем разрешения для теории и ее отраженного фрагмента остается открытым.

Логика доказательств LP С.Н. Артёмова [1], [2], [3], [5], [6] является примером разрешимой пропозициональной логики со свойством интернализации выводов. В языке LP присутствуют выражения двух видов — термы, или полиномы доказательств (proof polynomials), и формулы. Термы строятся из переменных и констант первого вида ("по доказательствам") с помощью унарной операции "!" (верификация) и бинарных операций "•" (аппликация, применение modus ponens),"+" (объединение доказательств). Формулы строятся из пропозициональных переменных (второго вида) с помощью булевых связок и дополнительного конструктора квазиатомарных формул ":", действующего по следующему правилу: если t — терм, a F — формула, то t:F является формулой.

Логика доказательств LP задается следующим исчислением: Аксиомы:

АО Аксиомы классической логики высказываний в языке LP, А1 t:F F,

А2 t:(F G) -> (s:F (t • s):G), A3 tF + s)F, sF + s)F, A4 tF->\t:{tF). Правила вывода :

MP) F G, F h G,

Nec) Ь с: А, где с — константа, а А — аксиома одного из видов А0-А4.

Забывающей проекцией называется перевод формул языка LP в модальный язык, получающийся в результате замены всех вхождений "t:" на модальность □. Как показано в работах [1], [3] (Теорема о реализуемости), забывающая проекция логики LP, т.е. образ множества всех теорем, совпадает с логикой абстрактной доказуемости S4 Гёделя. В этом смысле логику доказательств LP можно считать детализированным, или явным (explicit), вариантом S4.

Арифметическая семантика для языка LP описана в [1], [3]. Она позволяет интерпретировать символ ":" как многозначный предикат доказательств для формальной арифметики РА, т.е. как арифметическую Ai-формулу х есть код конечного множества, среди элементов которого есть РА-вывод формулы с кодом у".

При этом символам !,-,+ соответствуют вычислимые операции на конечных множествах выводов, специфицированные аксиомами А2-А4, а константам по доказательствам — конечные множества, содержащие РЛ-выводы арифметических переводов аксиом LP. В [3] доказано, что логика доказательств LP корректна и полна относительно арифметической семантики.

Как отмечено в [5], свойство интернализации выводов является фундаментальным свойством LP. Имеет место (см. [3]) эквивалентность:

LP I- F LP h t:F для некоторого терма t.

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

LP-выводов, в результате чего получается конечное множество, содержащее вывод формулы F. Эквивалентность не нарушится, если дополнительно потребовать, чтобы терм t не содержал переменные и операцию +, а операция ! применялась в нем только к константам. В этом случае структура (дерево подтермов) терма t изоморфна дереву вывода формулы F из аксиом А0-А4 с помощью правил (MP) и (Nec).

Разрешимость LP установлена в [16] с помощью развитой в этой работе техники символических моделей для логики доказательств. Оценка сложности разрешающего алгоритма из [16] получена в [12]: LP принадлежит классу Щ полиномиальной иерархии. Таким образом оказывается, что LP проще, чем ее забывающая проекция 54, т.к. последняя PSPACE-иолш [13]. Нетривиальной нижней оценки сложности LP неизвестно. До настоящей работы вопрос о сложности отраженного фрагмента логики LP, т.е. множества всех теорем LP вида t:F, также не был изучен.

Родственным LP примером типовой комбинаторной логики со свойством интернализации выводов является описанная в [5] рефлексивная комбинаторная логика RCI>. Она является расширением типовой комбинаторной логики CI„ (см. [19]), допускающим погружение суждений о типизации вида "t является термом типа F" в систему типов при помощи дополнительного конструктора типов t: F. Аналогичный конструктор типов присутствует в интуционистской теории типов (ITT, см. [9], [14]), но в этой теории типы вида t : F оказываются тривиальными в следующем смысле: каждый непустой ITT-тип t: F содержит единственный канонический элемент, один и тот же для всех типов такого вида. В отличие от ITT, непустой тип t: F в RCL> нетривиален. Как показывается в настоящей работе (см. главу 2), он населен термами t\ хранящими полную информацию о суждении "t является термом типа F", и само сужение может быть однозначно восстановлено как тип терма t'.

Для рефлексивной комбинаторной логики также справедлива (см. [5]) эквивалентность:

RCI» Ь F RCI> Ь t:F для некоторого терма t, причем по терму t из правой части удается однозначно восстановить формулу F и построить ее вывод (см. главу 2).

Приведем определение формальной системы RCL из [5]. В нем совместной индукцией определяются два суждения: "F есть правильно построенная формула (п.п.ф.)" и "F выводима из гипотез F\,., Fn". Правильно построенные формулы играют роль обозначений для типов. Суждение о выводимости можно интерпретировать как условное суждение "непустота типов Fi,.,Fn влечет непустоту F". Формализуемое этим суждением понятие выводимости использует единственное правило вывода modus ponens, причем постулировано, что все аксиомы есть п.п.ф., а правило modus ponens сохраняет свойство "быть п.п.ф.".

Язык RCL>, правильно построенные формулы и выводимые формулы определяются совместной индукцией.

1. Язык RCL-+ содержит пропозициональные переменные Po,Pi,.- и пропозициональную связку "—Каждая пропозициональная переменная есть (атомарная) формула.

2. Если S и Т — формулы, то S —* Т — также формула.

3. Для каждой формулы F фиксируется свой набор дока-зуемостных переменных xo,%i,. • ■ ■ Если х это переменная типа F, то x:F есть формула. Здесь и ниже утверждения "t:F есть формула" и "t есть терм типа F" используются как синонимы.

4. Каждая из аксиом А1-А6 является формулой.

А1. Для каждых формул А и t:A есть аксиома t:A А.

А2. Для каждой формулы А —(В —>■ А) фиксируется константа к и аксиома к : (А (В А)). A3. Для каждой формулы (А —► (В -> С)) ((А —> Б) —> (А —> С)) фиксируется константа s и аксиома s . [(i4 {В С)) ((Л В) (Л С))].

А4. Для каждой формулы —» Л фиксируется константа d и аксиома d : (Ы А).

А5. Если А, В, и : (А В), v : А — формулы, то (и • v) : В также формула, причем для формулы и:(А —> В) —» {v.А —» (и • v):B) фиксируется константа о и аксиома о : [и:(А В) ('и:А (и • *;):£)]. А6. Если А и t: А формулы, то ! t : t: А также формула, причем для формулы t:A —>\t:t:A фиксируется константа с и аксиома с : (Ы ->\t:t:A). 5. Каждая доказуемая из гипотез формула есть правильно построенная формула. Гипотезы — это произвольное конечное множество Г формул. Вывод из гипотез Г есть конечная последовательность формул, каждая из которых есть либо гипотеза из Г, либо аксиома, либо следует из предшествующих в данной последовательности по правилу modus ponens:

А->В А В '

Выражение Г b F означает, что существует вывод из Г, содержащий F"

Детальный анализ, некоторое уточнение и упрощение этого определения проделаны в главах 2, 3 настоящей работы. Сейчас же отметим, что в [5] отсутствовало явное определения типов и термов для системы RCI>, что оставляло открытым вопрос о том, что именно обозначают п.п.ф. До настоящей работы не были исследованы проблема разрешения и сложность логики RCI,, а также сложность задачи типизации термов ее средствами.

Целью работы является доказательство разрешимости и получение оценок сложности для ряда алгоритмических проблем, связанных с отраженным фрагментом RLP логики доказательств LP, рефлексивной комбинаторной логикой RCIее отраженным фрагментом и задачей типизации термов средствами RCIДля этого предложены простые дедуктивные описания RLP и RCIдопускающие эффективные алгоритмы поиска выводов формул.

Основные результаты работы таковы. •

• Пусть LP(CS') обозначает вариант логики доказательств LP с ограниченным правилом (Nec) — дополнительно требуется, чтобы его заключение принадлежало заданному конечному множеству формул CS. Показано, что отраженный фрагмент логики доказательств LP(CS') есть теория одной символической модели. В качестве следствий установлен ряд утверждений, упрощающих поиск выводов в LP, в частности, следующий вариант дизъюнктивного свойства:

LP Ь s:F V t:G & LP b s:F или LP h t:G.

• Установлено, что отраженный фрагмент логики доказательств LP принадлежит классу NP. Эта верхняя оценка ниже известной верхней оценки для всей логики LP. Аналогичная оценка доказана также для более широкого фрагмента — множества всех теорем LP, являющихся монотонными булевыми комбинациями квазиатомарных формул.

• Для рефлексивной комбинаторной логики RCI„ предложено явное определение типов. Доказана единственность типизации термов средствами RCI—Установлено, что задачи восстановления типов и проверки правильной построенности формул для RCI> разрешимы за полиномиальное время.

• Предложено секвенциальное исчисление, формализующее отношение выводимости из гипотез в рефлексивной комбинаторной логике RCL>. Показано, что правило сечения в нем устранимо. Отсюда следует, что отраженный фрагмент рефлексивной комбинаторной логики разрешим за полиномиальное время.

• Доказано, что отношение выводимости из гипотез в RCL разрешимо и PSPACE-полио.

Дальнейшее изложение придерживается следующего плана. Глава 1 посвящена изучению отраженного фрагмента RLP логики доказательств LP. Параграф 1.1 содержит определение символических моделей для языка логики доказательств и описание их основных свойств. В параграфе 1.2 доказывается существование наименьшей символической модели. Как следствие, устанавливается ограниченный вариант дизъюнктивного свойства логики доказательств. В параграфе 1.3 предлагается аксиоматическое описание отраженного фрагмента RLP логики доказательств LP. В параграфе 1.4 доказывается, что отраженный фрагмент логики доказательств RLP принадлежит классу сложности NP. Эта оценка распространяется также на более широкий класс теорем LP, имеющих вид монотонных булевых комбинаций квазиатомарных формул.

В главе 2 рассматривается задача типизации термов средствами рефлексивной комбинаторной логики RCI>. Параграфы 2.1, 2.2 посвящены упрощению определения правильно построенных формул языка RCL>. В параграфах 2.3, 2.4 предлагается явное определение типов для RCI, в виде отдельного исчисления RCLT-wf и показывается, что правильно построенные формулы являются корректными сокращенными обозначениями для типов. Устанавливается также, что все термы, входящие в состав правильно построенных формул, типизуемы единственным образом. В параграфе 2.5 рассматриваются проблемы типизации термов и восстановления типов в формулах. Доказывается, что обе они разрешимы за полиномиальное время.

Глава 3 посвящена изучению отношения выводимости из гипотез в рефлексивной комбинаторной логике. В параграфе 3.1 предлагается секвенциальная формулировка рефлексивной комбинаторной логики (исчисление RCLTg) и показывается ее эквивалентность исходному исчислению RCI—». В параграфе 3.2 устанавливается устранимость правила сечения в исчислении RCLTg- Параграфы 3.3 и 3.4 посвящены доказательству разрешимости отношения выводимости из гипотез в исчислении RCI—► и получению верхней оценки сложности (PSPACE) для разрешающего алгоритма. Эта оценка комбинируется с известной нижней оценкой сложности для импликативного фрагмента интуционистской пропозициональной логики, что позволяет доказать PSPACE-полноту проблемы выводимости для RCI— Здесь же доказывается, что отраженный фрагмент рефлексивной комбинаторной логики разрешим за полиномиальное время.

Автор выражает глубокую благодарность своему научному руководителю доктору физико-математических наук, профессору Владимиру Андреевичу Успенскому за постановку задачи и постоянное внимание к работе.

Похожие диссертационные работы по специальности «Математическая логика, алгебра и теория чисел», 01.01.06 шифр ВАК

Заключение диссертации по теме «Математическая логика, алгебра и теория чисел», Крупский, Николай Владимирович

Теорема 3.3.6 Множество секвенций, выводимых в исчислении

RCLTG, ^ отношение выводимости из гипотез в исчислении RCI >

разрешимы. Доказательство. Согласно лемме 3.3.3, секвенция V =^ F выводи ма в RCLTG тогда и только тогда, когда у секвенции set{V) =» F

существует монотонный RCLT'(^ -вывoд, в котором антецедент каждой

секвенции не содержит повторяющихся размеченных формул. Рас смотрим минимальный такой вывод. Он является последовательно стью секвенций, удовлетворяющих следующим условиям:

• все секвенции попарно различны и составлены из слабых под формул некоторых размеченных формул из множества Г U {F}

(лемма 3.3.5);

• кратность формул в антецедентах секвенций равна 1. Множество последовательностей, удовлетворяющих указанным усло виям, конечно и эффективно восстанавливается по секвенции Г =^ F.Для проверки ее выводимости достаточно выяснить, есть ли сре ди этих последовательностей монотонный КС1Т(^-вывод секвенции

set(r) => F. Согласно теореме 3.1.4, Г I-RCL_, F тогда и только тогда, когда 1)

все формулы из множества r u { F } правильно построены и 2) секвен ция Г'" => F^ обладает правильно построепным выводом в RCLTG. Первое из условий разрешимо по теореме 2.5.5, причем его выполне ние уже гарантирует суш,ествование и правильпую построенность се квенции Г^ =4> F''. Т.к. правило сечения в системе RCLTG устранимо,

то, по лемме 3.1.3, каждая выводимая в нем правильно построенная

секвенция имеет правильно построенный вывод тоже. Поэтому доста точно проверять лишь выводимость секвепции Г^ =^ JP^ в исчислении

RCLTG, ЧТО МОЖНО сделать изложенным выше методом. Замечание. Отметим, что результат о разрешимости (теорема 3.3.6)

может быть доказан тем же способом, основанным на более слабом

варианте леммы 3.3.3 (без условия монотонности и с более слабым

ограничением на кратность формул в антецедентах). Лемма 3.3.3 в

полном объеме будет использована ниже при доказательстве верхней

оценки сложности разрешаюш;их алгоритмов. 3.4 Оценки слож;ности. Покажем, что задача распознавания выводимости секвенций для ис числения RCLTG И задача распознавания выводимости из гипотез для

исчисления RCI > лежат в классе PSPACE. Онределение 3.4.1 Условимся называть размером секвенции сум му размеров всех входяш;их в нее размеченных формул. Лемма 3.4.2 Рассмотрим семейство всех минимальных монотон ных КаЛ^-выводов без повторяющихся размеченных формул в ан 72 тецедентах секвенций. Существуют полиномы qi и 2^ такие, что

глубина каждого из этих выводов не превосходит qi{n), а размеры

входящих в вывод секвенций не превосходят q2{n), где п — размер

выводимой секвенции. Доказательство. Возьмем произвольный КС1Т'(^-вывод секвенции размера п, удо влетворяющий условиям теоремы, и рассмотрим путь в дереве выво да от корня к листьям:

Разобьем этот путь на максимальные отрезки, внутри которых Г^

не меняется. Длина такого отрезка ограничена числом различных ва риантов для сукцедента, т.е. числом слабых подформул выводимой

секвенции, что не превосходит п. Количество отрезков разбиения не

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

длина пути ограничена величиной v?. Рассмотрим произвольную секвенцию из RCLTQ-вывода секвенции

размера п, удовлетворяющего условиям теоремы. Количество фор мул в ней ограничено величиной п + 1, поскольку антецедент не со держит повторений. Размер каждой формулы в данной секвенции

ограничен величиной п. Таким образом, размер секвенции ограни чен величиной п{п + 1). Теорема 3.4.3 Мноснсество всех выводимых в исчислении RCLTG

секвенций леоюит в классе PSPACE. Доказательство. Пусть qi,q2 — полиномы из леммы 3.4.2. Рассмот рим следующую игру двух лиц, (I) и (II). Начальной конфигурацией игры (6о) является секвенция Г =^ F размера п. Ходы игроков че редуются. Игрок (I) предлагает одну или две секвенции размера, не

превосходящего q2{Ti), а игрок (II) выбирает одну из них. Партия пре кращается, если игрок (II) выбрал аксиому исчисления RCLT'^ ^ или

количество ходов игрока (И) превысило qi{n). Пусть Wi - ходы иг рока (I), а bj - ходы игрока (П). Партия bQ,wi,bi,b2,W2,... считается

выигрыннюй для игрока (I), если выполнены условия:

1. Для каждого г фигура —— является монотонным частным

случаем одного из правил вывода исчисления

2. Кратность размеченных формул в антецеденте начальной се квенции и антецедентах всех секвенций, предлагаемых игроком

(I), равна единице. 3. Последний ход в игре является ходом игрока (II) и состоит в

выборе одной из аксиом исчисления RCLTQ. Количество ходов в игре и размер каждого хода, согласно лемме

3.4.2, полиномиально ограничены, а предикат выигрыша игрока (I)

вычислим за полиномиальное время. Из известной игровой характе ризации класса PSPACE (см. [10], [8]) следует, что для каждой такой

игры множество

Ji4 = {^ 0 I игрок (I) обладает выигрышной стратегией

в игре с начальной конфигурацией Ьо }

принадлежит классу PSPACE. Условие принадлежности множеству Л4 начальной конфигурации

Г => F эквивалентно выводимости в RCLTQ ЭТОЙ секвенции посред ством монотонного вывода без новторяющихся формул в антецеден тах. Поэтому лемма 3.3.3 устанавливает полиномиальную сводимость

множества всех выводимых в RCLTG секвенций к Л4. Это означа ет принадлежность множества всех выводимых в RCLTG секвенций

классу PSPACE.С л е д с т в и е 3.4.4 Проблема выводимости из гипотез в исчислении

RCI > лесисит в классе PSPACE. Доказательство. В доказательстве теоремы 3.3.6 ностроено ноли номиально ограниченное по времени сведение рассматриваемой за дачи к задаче выводимости секвенций в исчислении RCLTG. Теорема 3.4.5 Проблемы выводимости секвенций для исчисления

RCLTG и выводимости формул для исчисления RCI > являются

PSPACE-полными. Доказательство. Верхняя оценка сложности {PSPACE) для этих

двух задач установлена в теореме 3.4.3 и следствии 3.4.4 соответ ственно. Нижняя оценка {PSPACE-труддостъ) следует из извест ного результата Р. Статмана (см. [18]), установившего PSPACE-

полноту имнликативного фрагмента интуционистской логики выска зываний INT_>, т.е. множества всех имнликативных формул, являю щихся теоремами интуиционистской логики высказываний INT. Секвенциальная формулировка исчисления INT_+ состоит из всех

аксиом исчисления RCLTG, не содержащих термов, и нравил (Ь^),

(Я-*) и (L С). Поэтому все секвенции, выводимые в INT_ ,^ выводи мы также и в исчислении RCLTG. Из факта устранимости сечения в

RCLTG (теорема 3.2.5) следует, что обратное также верно. Кроме то го, каждая не содержащая термов формула F языка RCI > нравильно

построена и F^ = F, откуда RCL_^ \- F ^ RCLTG Ь {=^ F) но тео реме 3.1.4. Таким образом, для имнликативных пропозициональных

формул F справедливо

InthF ^ RCLTG h(=^F) ^ RCL_ h F.Это сведение переносит нижнюю оценку для INT_^ {PSРАСЕ трудность) на проблемы выводимости для исчислений RCLTG И

Таким образом, задача раснознавания выводимости формул из

гипотез для рефлексивной комбинаторной логики PSРАСE-пoлпгi,

причем нижняя оценка достигается уже в случае пустого множества

гинотез. Для сравнения оценим сложность отраженного фрагмента

рефлексивной комбинаторной логики, т.е. множества выводимых в

RCI > формул вида t:F. Лемма 3.4.6 RCI > h t:F тогда и только тогда, когда формула t:F

правильно построена и терм t не содержит переменных в качестве

подтермов. Доказательство. Пусть RCI > h t:F. По онределению выводимо сти в RCI >, формула t:F правильно построена. Тогда определена

размеченная формула {t:FY = {ty-.F^ и секвенция =^ {tY'.F^ выводи ма в исчислении RCLTG С ПОМОЩЬЮ правильно построенного вывода,

не использующего правило сечения (теоремы 3.1.4, 3.2.5). Индукци ей по длине такого вывода покажем, что размеченный терм {ty не

содержит размеченных подтермов-переменных. Последним правилом в выводе может быть только одно из правил

{R г), {R !) или {R •). В случае правила {Я г) единственным разме ченным нодтермом терма {ty = г^'^ является он сам. При этом г есть

идентификатор одной из констант, ноэтому {ty не является перемен ной. В случаях правил (Я !) и {Я •) утверждение непосредственно

следует из индуктивного предположения. При переводе (•)'' подтермы-переменные переходят в размеченные

подтермы-переменные, ноэтому у терма t нодтермов-переменных нет.Предположим теперь, что формула t: F правильно построена и

терм t не имеет подтермов-переменных. Тогда размеченная формула

{t: Fy =• {ty: F^ определена и является типом, причем размечен ный терм {ty не содержит размеченных подтермов-переменных. Ин дукцией по выводу в исчислении RCLT-wf суждения "(i:F)' ' - тип"

покажем, что секвенция => {t: Fy выводима в исчислении RCLTG

без правила сечения. Такой вывод будет правильно построенным по

лемме 3.1.3, откуда RCI > h t:F согласно теореме 3.1.4. Последним правилом в выводе суждения ^^{t:Fy - тип" может

быть только одно из правил 4 - 1 0 исчислепия RCLT-wf. В случае

правил 4, 5, 6, 8, 10 терм {ty оказывается константой и секвенцию

=^ {t:Fy удается вывести в RCLTG ПО правилу (Л г). Для правил 7

и 9 достаточно воспользоваться индуктивным предположением для

построения выводов секвенций, соответствующих посылкам, и про должить эти выводы применением одного из правил {R •) или (Я !). в качестве следствия получим следующую оценку. Теорема 3.4.7 Задача распознавания выводимости формул вида

tiF в исчислении RCI > разрешима за полиномиальное время (от

размера формулы). Доказательство. Лемма 3.4.6 за полиномиальное время сводит за дачу распознавание выводимости формулы t:F к проверке ее пра вильной построенности. Последняя разрешима за полиномиальное

время согласно теореме 2.5.5.

Список литературы диссертационного исследования кандидат физико-математических наук Крупский, Николай Владимирович, 2006 год

1. S. Artemov. Operational Modal Logic. Technical Report MS1.95-29, Cornell University, 1995.

2. S. Artemov. Logic of proofs: a unified semantics for modality and A-terms. Technical Report CFIS 98-06, Cornell University, 1998

3. S. Artemov. Explicit provability and constructive semantics. The Bulletin of Symbolic Logic, 7(l):l-36, 2001.

4. S. Artemov. Unified semantics for modality and lambda-terms via proof polynomials. In: Kees Vermeulen and Ann Copestake eds., Algebras, Diagrams and Decisions in Language, Logic and Computation, CSLI Publications, Stanford University, 2002.

5. С. Артемов. Подход Колмогорова и Геделя к интуиционистской логике и работы последнего десятилетия в этом направлении. Успехи матем. наук, 2004, 59, вып. 2 (356), 9-36.

6. S.Artemov, L.Beklemishev. Provability logic. In D.Gabbay, F.Guenthner, eds., Handbook of Philosophical Logic, 2nd ed., v. 13, 229-403, Kluwer, Dordrecht, 2004.

7. M. Bidoit, J. Corbin. A Rehabilitation of Robinson's Unification Algorithm. Information Processing, 83:909-914, 1983.

8. A.K. Chandra, D.C. Kozen, L.J. Stockmeyer. Alternation. J. Assoc. Comput. Mach., v. 28, 1981, pp 114-133.

9. R.L. Constable. Types in logic, mathematics and programming. In S.R. Buss, ed., Handbook of proof theory, chapter X, Elsevier Science B.V., 1998, pp. 684-786.

10. А. Китаев, А. Шень, M. Вялый. Классические и квантовые вычисления. М.: МЦНМО, ЧеРо, 1999.

11. С.К. Клини. Введение в метаматематику. М.: ИЛ, 1957.

12. R. Kuznets. On the complexity of explicit modal logics. In Computer Science Logic 2000, volume 1862 of Lecture Notes in Computer Science, pages 371-383. Springer-Verlag, 2000.

13. R. Ladner. The computational complexity of provability in systems of modal logic. SIAM Journal of Computing, v.6 (3), 1977, pp. 467480.

14. P. Martin-Lof. An intuitionistic theory of types. In G. Sambin, J. Smith, eds., Twenty five years of Constructive Type Theory, Oxford Logic Guides, v. 36, 1998, pp. 127-172.

15. Э. Мендельсон. Введение в математическую логику. М.: Наука, 1976.

16. A. Mkrtychev. Models for the logic of proofs. Lecture Notes in Computer Science, v. 1234, 266-275. Springer, 1997.

17. J.A. Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, v. 12, n. 1, 1965, pp. 23-41.

18. R. Statman. Intuitionistic propositional logic is polynomial-space complete. Theoretical Comput. Sci. 9, 1979, pp. 67-72

19. A. S. Troelstra, H. Schwichtenberg. Basic proof theory. Cambridge: Cambridge Univ. Press, 1996.Работы автора по теме диссертации

20. Н.В. Крупский. О сложности фрагментов логики доказательств. В сб.: Труды XXIV Конференции молодых ученых механико-математического факультета МГУ им. М.В. Ломоносова, 2002, 96-98.

21. N. Krupski. On the complexity of the reflected logic of proofs. CUNY Ph.D Program in CS Technical Reports, TR-2003007, 2003, 12 p. http://www.es.gc.cuny.edu/tr/techreport.php?id=81

22. Н.В. Крупский. О синтаксисе рефлексивной комбинаторной логики. Деп. в ВИНИТИ, №412-В2005, М. ВИНИТИ, 2005, 29 с.

23. N. Krupski. Typing in Reflective Combinatory Logic. CUNY Ph.D Program in CS Technical Reports, TR-2005013, 2005, 24 p. http://www.es.gc.cuny.edu/tr/techreport.php?id=166

24. Н.В. Крупский. Минимальные модели и сложность фрагментов логики доказательств. Вестник МГУ, сер. 1., Математика, Механика, 2006, №1. 52-53.

Обратите внимание, представленные выше научные тексты размещены для ознакомления и получены посредством распознавания оригинальных текстов диссертаций (OCR). В связи с чем, в них могут содержаться ошибки, связанные с несовершенством алгоритмов распознавания. В PDF файлах диссертаций и авторефератов, которые мы доставляем, подобных ошибок нет.