Сложность доказательства

В логике и теоретической информатике , в частности в теории доказательств и теории сложности вычислений , сложность доказательства — это область, целью которой является понимание и анализ вычислительных ресурсов, которые необходимы для доказательства или опровержения утверждений. Исследования сложности доказательства в основном связаны с доказательством нижних и верхних границ длины доказательства в различных системах пропозициональных доказательств . Например, одной из основных проблем сложности доказательства является доказательство того, что система Фреге , обычное исчисление высказываний , не допускает доказательств полиномиального размера для всех тавтологий. Здесь размер доказательства — это просто количество символов в нем, и говорят, что доказательство имеет полиномиальный размер, если оно полиномиально по размеру доказываемой им тавтологии.

Систематическое изучение сложности доказательства началось с работы Стивена Кука и Роберта Рекхоу (1979), которые дали базовое определение системы пропозициональных доказательств с точки зрения вычислительной сложности. В частности, Кук и Рекхау заметили, что доказательство нижних границ размера доказательства для все более и более сильных систем пропозициональных доказательств можно рассматривать как шаг к отделению NP от coNP (и, следовательно, P от NP), поскольку существование системы пропозициональных доказательств, которая допускает доказательства полиномиального размера для всех тавтологий эквивалентно NP=coNP.

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

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

Системы доказательств [ править ]

Система пропозиционального доказательства представлена как алгоритм проверки доказательства P ( A , x ) с двумя входами. Если P принимает пару ( A , x мы говорим, что x является P -доказательством A. ) , P Требуется, чтобы выполнялся за полиномиальное время, и, более того, должно выполняться утверждение, что A имеет P -доказательство тогда и только тогда, когда A является тавтологией.

Примеры систем доказательства высказываний включают секвенционное исчисление , резолюцию , секущие плоскости и системы Фреге . Сильные математические теории, такие как ZFC, также порождают системы пропозициональных доказательств: доказательство тавтологии. $\tau$ в пропозициональной интерпретации ZFC является ZFC-доказательством формализованного утверждения' $\tau$ есть тавтология».

NP и coNP размера полинома Доказательства и проблема

Сложность доказательства обычно измеряет эффективность системы доказательств с точки зрения минимального размера доказательств, возможных в системе для данной тавтологии. Размер доказательства (соответственно формулы) — это количество символов, необходимых для представления доказательства (соответственно формулы). Система пропозициональных доказательств P если полиномиально ограничена, существует константа $c$ такие, что каждая тавтология размера $n$ имеет P -доказательство размера $(n+c)^{c}$ . Центральный вопрос сложности доказательства — понять, допускают ли тавтологии доказательства полиномиального размера. Формально,

Проблема (NP против coNP)
Существует ли полиномиально ограниченная система доказательства высказываний?

Кук и Рекхоу (1979) заметили, что существует полиномиально ограниченная система доказательств тогда и только тогда, когда NP = coNP. Следовательно, доказательство того, что конкретные системы доказательств не допускают доказательств полиномиального размера, можно рассматривать как частичный прогресс на пути к разделению NP и coNP (и, следовательно, P и NP). ^[1]

Оптимальность и моделирование доказательства между системами

Сложность доказательства сравнивает силу систем доказательства с использованием понятия моделирования. Система доказательств P p-моделирует систему доказательств Q, если существует функция с полиномиальным временем, которая при Q -доказательстве тавтологии выводит P -доказательство той же тавтологии. Если P p-моделирует Q , а Q p-моделирует P , то системы доказательств P и Q эквивалентны p- . Существует также более слабое понятие моделирования: система доказательств P моделирует систему доказательств Q, если существует полином p такой, что для каждого Q -доказательства x тавтологии A существует P -доказательство y из A такое, что длина из y , | й | не превосходит p (| x |).

Например, секвенциальное исчисление p-эквивалентно (любой) системе Фреге. ^[2]

Система доказательств p-оптимальна, если она p -моделирует все другие системы доказательств, и оптимальна, если она моделирует все другие системы доказательств. Существуют ли такие системы доказательств — открытый вопрос:

Проблема (Оптимальность)
Существует ли p-оптимальная или оптимальная система доказательства высказываний?

Любую систему доказательства высказываний P можно смоделировать с помощью расширенного Фреге, дополненного аксиомами, постулирующими правильность P . ^[3] Известно, что существование оптимальной (соответственно p-оптимальной) системы доказательств следует из предположения, что NE=coNE (соответственно E = NE ). ^[4]

Известно, что многие системы слабых доказательств не моделируют некоторые более сильные системы (см. ниже). Однако вопрос остается открытым, если понятие моделирования смягчить. Например, неизвестно, эффективно ли Разрешение полиномиально моделирует Расширенный Фреге. ^[5]

Автоматизация поиска доказательств [ править ]

Важным вопросом сложности доказательства является понимание сложности поиска доказательств в системах доказательств.

Проблема (автоматизация)
Существуют ли эффективные алгоритмы поиска доказательств в стандартных системах доказательств, таких как Резолюция или система Фреге?

Вопрос можно формализовать с помощью понятия автоматизируемости (также известной как автоматизируемость). ^[6]

Система доказательства P является автоматизированной , если существует алгоритм, который дает тавтологию $\tau$ выводит P -доказательство $\tau$ полиномиально по времени по размеру $\tau$ и длина кратчайшего P -доказательства $\tau$ . Обратите внимание: если система доказательства не является полиномиально ограниченной, ее все равно можно автоматизировать. Система доказательств P является слабо автоматизируемой , если существуют система доказательств R и алгоритм, который дает тавтологию $\tau$ выводит R -доказательство $\tau$ полиномиально по времени по размеру $\tau$ и длина кратчайшего P -доказательства $\tau$ .

Считается, что многие представляющие интерес системы доказательств неавтоматизируются. Однако на данный момент известны лишь условно-отрицательные результаты.

Крайчек и Пудлак (1998) доказали, что Extended Frege не является слабо автоматизируемым, если только RSA не защищен от P/poly . ^[7]
Боне , Питасси и Раз (2000) доказали, что $TC^{0}$ -Система Фреге не является слабо автоматизируемой, если только схема Диффи-Хеллмана не защищена от P/poly. ^[8] Это было расширено Боне, Доминго, Гавальдой, Масиелем и Питасси (2004), которые доказали, что системы Фреге постоянной глубины с глубиной не менее 2 не являются слабо автоматизируемыми, если только схема Диффи-Хеллмана не защищена от неоднородных противников, работающих в субэкспоненциальном времени. ^[9]
Алехнович и Разборов (2008) доказали, что древовидное разрешение и разрешение невозможно автоматизировать, если только FPT=W[P] . ^[10] Это было расширено Галези и Лаурией (2010), которые доказали, что Nullstellensatz и полиномиальное исчисление невозможно автоматизировать, если иерархия с фиксированными параметрами не рухнет. ^[11] Мерц, Питасси и Вей (2019) доказали, что древовидное разрешение и разрешение невозможно автоматизировать даже в определенное квазиполиномиальное время, предполагая гипотезу экспоненциального времени . ^[12]
Ацериас и Мюллер (2019) доказали, что разрешение невозможно автоматизировать, если P = NP. ^[13] Это было распространено де Резенде, Гёосом, Нордстремом, Питасси, Робером и Соколовым (2020) на NP-трудность автоматизации теоремы о нулевой точке и полиномиального исчисления; ^[14] Гёосом, Коротом, Мерцем и Питасси (2020) к NP-трудности автоматизации секущих плоскостей; ^[15] и Гарлика (2020) к NP-трудности автоматизации разрешения k - DNF . ^[16]

Неизвестно, нарушит ли слабая автоматизация разрешения какие-либо стандартные предположения о сложности теории сложности.

С положительной стороны,

Бим и Питасси (1996) показали, что древовидное разрешение автоматизируется за квазиполиномиальное время, а разрешение автоматизируется по формулам небольшой ширины за слабо субэкспоненциальное время. ^[17]^[18]

Ограниченная арифметика [ править ]

Системы пропозициональных доказательств можно интерпретировать как неоднородные эквиваленты теорий более высокого порядка. Эквивалентность чаще всего изучается в контексте теорий ограниченной арифметики . Например, расширенная система Фреге соответствует теории Кука. $\mathrm {PV} _{1}$ формализация рассуждений за полиномиальное время, и система Фреге соответствует теории $\mathrm {VNC} ^{1}$ формализация ${\mathsf {NC}}^{1}$ рассуждения.

Соответствие было введено Стивеном Куком (1975), который показал, что теоремы coNP формально $\Pi _{1}^{b}$ формулы теории $\mathrm {PV} _{1}$ перевести в последовательности тавтологий с доказательствами полиномиального размера в расширенном Фреге. Более того, расширенная система Фреге является самой слабой такой системой: если другая система доказательств P обладает этим свойством, то P имитирует расширенную систему Фреге. ^[19]

Альтернативный перевод утверждений второго порядка и пропозициональных формул, предложенный Джеффом Пэрисом и Алексом Уилки (1985), оказался более практичным для описания подсистем расширенного Фреге, таких как Фреге или Фреге постоянной глубины. ^[20]^[21]

Хотя вышеупомянутое переписка гласит, что доказательства в теории преобразуются в последовательности коротких доказательств в соответствующей системе доказательств, имеет место и форма противоположной импликации. Можно получить нижние оценки размера доказательств в системе доказательств P, построив подходящие модели теории T, соответствующие системе P . Это позволяет доказывать нижние границы сложности с помощью теоретико-модельных конструкций - подхода, известного как метод Айтая . ^[22]

Решатели SAT [ править ]

Системы пропозициональных доказательств можно интерпретировать как недетерминированные алгоритмы распознавания тавтологий. Таким образом, доказательство суперполиномиальной нижней границы системы доказательств P исключает существование алгоритма с полиномиальным временем для SAT, основанного на P . Например, запуск алгоритма DPLL на неудовлетворительных экземплярах соответствует древовидному опровержению Резолюции. Следовательно, экспоненциальные нижние границы древовидного разрешения (см. ниже) исключают существование эффективных алгоритмов DPLL для SAT. Аналогичным образом, нижние границы экспоненциального разрешения подразумевают, что решатели SAT, основанные на разрешении, такие как алгоритмы CDCL, не могут эффективно решать SAT (в худшем случае).

Нижние границы [ править ]

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

Хакен (1985) доказал экспоненциальную нижнюю границу разрешения и принцип «ячейки». ^[23]
Айтай (1988) доказал суперполиномиальную нижнюю оценку для системы Фреге постоянной глубины и принципа «ячейки». ^[24] Крайчек, Пудлак и Вудс усилили это значение до экспоненциальной нижней границы. ^[25] и Питасси, Биме и Импальяццо. ^[26] Нижняя оценка Аджтая использует метод случайных ограничений, который также использовался для получения AC ⁰ нижние границы сложности схемы .
Кружево (1994) ^[27] сформулировал метод допустимой интерполяции и позже использовал его для получения новых нижних оценок разрешения и других систем доказательства. ^[28]
Пудлак (1997) доказал экспоненциальные нижние оценки для секущих плоскостей с помощью допустимой интерполяции. ^[29]
Бен-Сассон и Вигдерсон (1999) предложили метод доказательства, уменьшающий нижние границы размера опровержений Резолюции до нижних границ ширины опровержений Резолюции, который отражает многие обобщения нижней границы Хакена. ^[18]

Получение нетривиальной нижней оценки для системы Фреге является давней открытой проблемой.

Возможная интерполяция

Рассмотрим тавтологию вида $A(x,y)\rightarrow B(y,z)$ . Тавтология верна для любого выбора $y$ , и после исправления $y$ оценка $A$ и $B$ независимы, поскольку они определены на непересекающихся множествах переменных. Это означает, что можно определить интерполянтную схему $C(y)$ , такой, что оба $A(x,y)\rightarrow C(y)$ и $C(y)\rightarrow B(y,z)$ держать. Интерполянтная схема решает: $A(x,y)$ ложно или если $B(y,z)$ верно, только учитывая $y$ . Характер интерполянтной схемы может быть произвольным. Тем не менее можно воспользоваться доказательством исходной тавтологии $A(x,y)\rightarrow B(y,z)$ как подсказка о том, как построить $C$ . система доказательств P Говорят, что имеет допустимую интерполяцию, если интерполянт $C(y)$ эффективно вычислимо из любого доказательства тавтологии $A(x,y)\rightarrow B(y,z)$ в П. Эффективность измеряется длиной доказательства: для более длинных доказательств легче вычислять интерполянты, поэтому это свойство кажется антимонотонным с точки зрения силы системы доказательств.

Следующие три утверждения не могут быть одновременно истинными: (а) $A(x,y)\rightarrow B(y,z)$ имеет краткое доказательство в некоторой системе доказательств; (b) такая система доказательств имеет допустимую интерполяцию; (c) схема интерполяции решает сложную вычислительную задачу. Ясно, что (а) и (б) подразумевают наличие небольшой интерполянтной схемы, что противоречит (в). Такое соотношение позволяет преобразовать верхние границы длины доказательства в нижние границы вычислений и двойным образом превратить эффективные алгоритмы интерполяции в нижние границы длины доказательства.

Некоторые системы доказательства, такие как разрешение и секущие плоскости, допускают допустимую интерполяцию или ее варианты. ^[28]^[29]

Возможную интерполяцию можно рассматривать как слабую форму автоматизации. Фактически, для многих систем доказательств, таких как расширенная система Фреге, допустимая интерполяция эквивалентна слабой автоматизируемости. В частности, многие системы доказательства P способны доказать свою надежность, что является тавтологией. $\mathrm {Ref} _{P}(\pi ,\phi ,x)$ заявив, что «если $\pi$ является P -доказательством формулы $\phi (x)$ затем $\phi (x)$ держит». Здесь, $\pi ,\phi ,x$ кодируются свободными переменными. Более того, можно генерировать P -доказательства $\mathrm {Ref} _{P}(\pi ,\phi ,x)$ за полиномиальное время, учитывая длину $\pi$ и $\phi$ . Следовательно, эффективный интерполянт, полученный в результате коротких P -доказательств правильности P, будет решать, является ли данная формула $\phi$ допускает короткое P -доказательство $\pi$ . Такой интерполянт можно использовать для определения системы доказательства R, свидетельствующей о том, что P слабо автоматизируема. ^[30] С другой стороны, из слабой автоматизируемости системы доказательств P следует, что P допускает допустимую интерполяцию. Однако если система доказательства P не доказывает эффективно свою надежность, то она не может быть слабо автоматизируемой, даже если допускает допустимую интерполяцию.

Многие результаты неавтоматизируемости свидетельствуют против возможности интерполяции в соответствующих системах.

Крайчек и Пудлак (1998) доказали, что расширенный Фреге не допускает осуществимой интерполяции, если RSA не защищен от P/poly. ^[31]
Боне, Питасси и Раз (2000) доказали, что $TC^{0}$ -Система Фреге не допускает осуществимой интерполяции, если только схема Диффи-Хельмана не защищена от P/poly. ^[32]
Боне, Доминго, Гавальда, Масиэль, Питасси (2004) доказали, что системы Фреге постоянной глубины не допускают осуществимой интерполяции, если только схема Диффи-Хельмана не защищена от неоднородных противников, работающих в субэкспоненциальном времени. ^[33]

Неклассическая логика [ править ]

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

Грубеш (2007–2009) доказал экспоненциальные нижние границы размера доказательств в расширенной системе Фреге в некоторых модальных логиках и в интуиционистской логике, используя версию монотонной допустимой интерполяции. ^[34]^[35]^[36]

См. также [ править ]

Ссылки [ править ]

^ Кук, Стивен ; Рекхау, Роберт А. (1979). «Относительная эффективность систем доказательства высказываний». Журнал символической логики . 44 (1): 36–50. дои : 10.2307/2273702 . JSTOR 2273702 . S2CID 2187041 .
^ Рекхау, Роберт А. (1976). О длинах доказательств в исчислении высказываний (кандидатская диссертация). Университет Торонто.
^ Крайчек, Ян (2019). Сложность доказательства . Издательство Кембриджского университета.
^ Крайчек, Ян; Пудлак, Павел (1989). «Пропозициональные системы доказательства, непротиворечивость теорий первого порядка и сложность вычислений». Журнал символической логики . 54 (3): 1063–1079. дои : 10.2307/2274765 . JSTOR 2274765 . S2CID 15093234 .
^ Питасси, Тонианн ; Сантанам, Рахул (2010). «Эффективно полиномиальное моделирование» (PDF) . ИКС : 370–382.
^ Бонет, ML ; Питасси, Тонианн ; Раз, Ран (2000). «Об интерполяции и автоматизации системы доказательств Фреге». SIAM Journal по вычислительной технике . 29 (6): 1939–1967. дои : 10.1137/S0097539798353230 .
^ Крайчек, Ян; Пудлак, Павел (1998). «Некоторые следствия криптографических гипотез для $S_{2}^{1}$ и EF» . Information and Computing . 140 (1): 82–94. doi : 10.1006/inco.1997.2674 .
^ Бонет, ML ; Питасси, Тонианн ; Раз, Ран (2000). «Об интерполяции и автоматизации системы доказательств Фреге». SIAM Journal по вычислительной технике . 29 (6): 1939–1967. дои : 10.1137/S0097539798353230 .
^ Бонет, ML ; Доминго, К.; Гавальда, Р.; Масиэль, А.; Питасси, Тонианн (2004). «Неавтоматизируемость доказательств Фреге ограниченной глубины». Вычислительная сложность . 13 (1–2): 47–68. дои : 10.1007/s00037-004-0183-5 . S2CID 1360759 .
^ Алехнович, Михаил; Разборов, Александр (2018). «Разрешение невозможно автоматизировать, если W[P] не является управляемым». SIAM Journal по вычислительной технике . 38 (4): 1347–1363. дои : 10.1137/06066850X .
^ Галези, Никола; Лаурия, Массимо (2010). «Об автоматизации полиномиального исчисления». Теория вычислительных систем . 47 (2): 491–506. дои : 10.1007/s00224-009-9195-5 . S2CID 11602606 .
^ Мерц, Ян; Питасси, Тонианн; Вэй, Юаньхао (2019). «Короткие доказательства трудно найти». ИКАЛП .
^ Ацериас, Альберт ; Мюллер, Мориц (2019). «Автоматизация разрешения NP-сложна». Материалы 60-го симпозиума по основам информатики . стр. 498–509.
^ де Резенде, Сюзанна; Гёос, Мика; Нордстрем, Якоб; Питасси, Тонниан; Робер, Роберт; Соколов, Дмитрий (2020). «Автоматизация алгебраических систем доказательства NP-сложна». ЕССС .
^ Гёос, Мика; Корот, Саджин; Мерц, Ян; Питасси, Тонниан (2020). «Автоматизация плоскостей разреза NP-сложна». Материалы 52-го ежегодного симпозиума ACM SIGACT по теории вычислений . стр. 68–77. arXiv : 2004.08037 . дои : 10.1145/3357713.3384248 . ISBN 9781450369794 . S2CID 215814356 . {{cite book}}: CS1 maint: дата и год ( ссылка )
^ Гарлик, Михал (2020). «Недостаток допустимого свойства дизъюнкции для разрешения k -ДНФ и NP-трудность его автоматизации». ЕССС . arXiv : 2003.10230 .
^ Бим, Пол ; Питасси, Тонианн (1996). «Упрощенные и улучшенные нижние границы разрешения». 37-й ежегодный симпозиум по основам информатики : 274–282.
↑ Перейти обратно: Перейти обратно: ^а ^б Бен-Сассон, Эли ; Вигдерсон, Ави (1999). «Краткие доказательства узки - решение упрощено». Материалы 31-го симпозиума ACM по теории вычислений . стр. 517–526.
^ Кук, Стивен (1975). «Возможно конструктивные доказательства и исчисление предложений». Материалы 7-го ежегодного симпозиума ACM по теории вычислений . стр. 83–97.
^ Пэрис, Джефф ; Уилки, Алекс (1985). «Задачи подсчета в ограниченной арифметике». Методы математической логики . Конспект лекций по математике. Том. 1130. стр. 317–340. дои : 10.1007/BFb0075316 . ISBN 978-3-540-15236-1 .
^ Кук, Стивен ; Нгуен, Фуонг (2010). Логические основы сложности доказательства . Перспективы в логике. Кембридж: Издательство Кембриджского университета. дои : 10.1017/CBO9780511676277 . ISBN 978-0-521-51729-4 . МР 2589550 . ( проект 2008 года )
^ Аджтай, М. (1988). «Сложность принципа сортировки». Труды 29-го ежегодного симпозиума IEEE по основам компьютерных наук . стр. 346–355.
^ Хакен, А. (1985). «Неразрешимость разрешения». Теоретическая информатика . 39 : 297–308. дои : 10.1016/0304-3975(85)90144-6 .
^ Аджтай, М. (1988). «Сложность принципа сортировки». Труды 29-го ежегодного симпозиума IEEE по основам компьютерных наук . стр. 346–355.
^ Крайчек, Ян; Пудлак, Павел ; Вудс, Алан (1995). «Экспоненциальная нижняя граница размера ограниченной глубины. Доказательства Фреге принципа голубиной норы». Случайные структуры и алгоритмы . 7 (1): 15–39. дои : 10.1002/rsa.3240070103 .
^ Питасси, Тонианн ; Бим, Пол ; Импальяццо, Рассел (1993). «Экспоненциальные нижние оценки принципа группировки». Вычислительная сложность . 3 (2): 97–308. дои : 10.1007/BF01200117 . S2CID 1046674 .
^ Крайчек, Ян (1994). «Нижние границы размера доказательств высказываний постоянной глубины». Журнал символической логики . 59 (1): 73–86. дои : 10.2307/2275250 . JSTOR 2275250 . S2CID 44670202 .
↑ Перейти обратно: Перейти обратно: ^а ^б Крайчек, Ян (1997). «Интерполяционные теоремы, нижние оценки для систем доказательств и результаты о независимости для ограниченной арифметики». Журнал символической логики . 62 (2): 69–83. дои : 10.2307/2275541 . JSTOR 2275541 . S2CID 28517300 .
↑ Перейти обратно: Перейти обратно: ^а ^б Пудлак, Павел (1997). «Нижние оценки разрешения, доказательства секущих плоскостей и монотонные вычисления». Журнал символической логики . 62 (3): 981–998. дои : 10.2307/2275583 . JSTOR 2275583 . S2CID 8450089 .
^ Пудлак, Павел (2003). «О сводимости и симметрии непересекающихся NP-пар». Теоретическая информатика . 295 : 323–339. дои : 10.2307/2275583 . JSTOR 2275583 . S2CID 8450089 .
^ Крайчек, Ян; Пудлак, Павел (1998). «Некоторые следствия криптографических гипотез для $S_{2}^{1}$ и EF» . Information and Computing . 140 (1): 82–94. doi : 10.1006/inco.1997.2674 .
^ Бонет, ML ; Питасси, Тонианн ; Раз, Ран (2000). «Об интерполяции и автоматизации системы доказательств Фреге». SIAM Journal по вычислительной технике . 29 (6): 1939–1967. дои : 10.1137/S0097539798353230 .
^ Бонет, ML ; Доминго, К.; Гавальда, Р.; Масиэль, А.; Питасси, Тонианн (2004). «Неавтоматизируемость доказательств Фреге ограниченной глубины». Вычислительная сложность . 13 (1–2): 47–68. дои : 10.1007/s00037-004-0183-5 . S2CID 1360759 .
^ Грубеш, Павел (2007). «Нижние границы модальной логики». Журнал символической логики . 72 (3): 941–958. дои : 10.2178/jsl/1191333849 . S2CID 1743011 .
^ Грубеш, Павел (2007). «Нижняя граница интуиционистской логики». Анналы чистой и прикладной логики . 146 (1): 72–90. дои : 10.1016/j.apal.2007.01.001 .
^ Грубеш, Павел (2009). «О длинах доказательств в неклассической логике» . Анналы чистой и прикладной логики . 157 (2–3): 194–205. дои : 10.1016/j.apal.2008.09.013 .

Дальнейшее чтение [ править ]

Бим, Пол; Питасси, Тонианн (1998), «Сложность доказательства высказываний: прошлое, настоящее и будущее», Бюллетень Европейской ассоциации теоретической информатики , 65 : 66–89, MR 1650939 , ECCC TR98-067
Кук, Стивен ; Нгуен, Фуонг (2010), Логические основы сложности доказательств , Перспективы логики, Кембридж: Издательство Кембриджского университета, doi : 10.1017/CBO9780511676277 , ISBN 978-0-521-51729-4 , МР 2589550 ( проект от 2008 г. )
Крайичек, Ян (1995), Ограниченная арифметика, логика высказываний и теория сложности , Cambridge University Press
Крайчек, Ян (2005), «Сложность доказательства» (PDF) , в Лаптеве А. (ред.), Труды 4-го Европейского математического конгресса , Цюрих: Европейское математическое общество, стр. 221–231, MR 2185746
Крайчек, Ян, Сложность доказательства , Cambridge University Press, 2019.
Пудлак, Павел (1998), «Длина доказательств», в Буссе, С.Р. (ред.), Справочник по теории доказательств , Исследования по логике и основам математики, том. 137, Амстердам: Северная Голландия, стр. 547–637, номер документа : 10.1016/S0049-237X(98)80023-2 , MR 1640332.

Внешние ссылки [ править ]

[cr-1] Кук, Стивен ; Рекхау, Роберт А. (1979). «Относительная эффективность систем доказательства высказываний». Журнал символической логики . 44 (1): 36–50. дои : 10.2307/2273702 . JSTOR 2273702 . S2CID 2187041 .

[Rec-2] Рекхау, Роберт А. (1976). О длинах доказательств в исчислении высказываний (кандидатская диссертация). Университет Торонто.

[Kpc-3] Крайчек, Ян (2019). Сложность доказательства . Издательство Кембриджского университета.

[KP1-4] Крайчек, Ян; Пудлак, Павел (1989). «Пропозициональные системы доказательства, непротиворечивость теорий первого порядка и сложность вычислений». Журнал символической логики . 54 (3): 1063–1079. дои : 10.2307/2274765 . JSTOR 2274765 . S2CID 15093234 .

[PS-5] Питасси, Тонианн ; Сантанам, Рахул (2010). «Эффективно полиномиальное моделирование» (PDF) . ИКС : 370–382.

[BPR-6] Бонет, ML ; Питасси, Тонианн ; Раз, Ран (2000). «Об интерполяции и автоматизации системы доказательств Фреге». SIAM Journal по вычислительной технике . 29 (6): 1939–1967. дои : 10.1137/S0097539798353230 .

[KP-7] Крайчек, Ян; Пудлак, Павел (1998). «Некоторые следствия криптографических гипотез для $S_{2}^{1}$ и EF» . Information and Computing . 140 (1): 82–94. doi : 10.1006/inco.1997.2674 .

[BPRc-8] Бонет, ML ; Питасси, Тонианн ; Раз, Ран (2000). «Об интерполяции и автоматизации системы доказательств Фреге». SIAM Journal по вычислительной технике . 29 (6): 1939–1967. дои : 10.1137/S0097539798353230 .

[BDGMP-9] Бонет, ML ; Доминго, К.; Гавальда, Р.; Масиэль, А.; Питасси, Тонианн (2004). «Неавтоматизируемость доказательств Фреге ограниченной глубины». Вычислительная сложность . 13 (1–2): 47–68. дои : 10.1007/s00037-004-0183-5 . S2CID 1360759 .

[AleRaz-10] Алехнович, Михаил; Разборов, Александр (2018). «Разрешение невозможно автоматизировать, если W[P] не является управляемым». SIAM Journal по вычислительной технике . 38 (4): 1347–1363. дои : 10.1137/06066850X .

[GaLa-11] Галези, Никола; Лаурия, Массимо (2010). «Об автоматизации полиномиального исчисления». Теория вычислительных систем . 47 (2): 491–506. дои : 10.1007/s00224-009-9195-5 . S2CID 11602606 .

[MPW-12] Мерц, Ян; Питасси, Тонианн; Вэй, Юаньхао (2019). «Короткие доказательства трудно найти». ИКАЛП .

[AM-13] Ацериас, Альберт ; Мюллер, Мориц (2019). «Автоматизация разрешения NP-сложна». Материалы 60-го симпозиума по основам информатики . стр. 498–509.

[RGNPRS-14] де Резенде, Сюзанна; Гёос, Мика; Нордстрем, Якоб; Питасси, Тонниан; Робер, Роберт; Соколов, Дмитрий (2020). «Автоматизация алгебраических систем доказательства NP-сложна». ЕССС .

[GKMP-15] Гёос, Мика; Корот, Саджин; Мерц, Ян; Питасси, Тонниан (2020). «Автоматизация плоскостей разреза NP-сложна». Материалы 52-го ежегодного симпозиума ACM SIGACT по теории вычислений . стр. 68–77. arXiv : 2004.08037 . дои : 10.1145/3357713.3384248 . ISBN 9781450369794 . S2CID 215814356 . {{cite book}}: CS1 maint: дата и год ( ссылка )

[Gar-16] Гарлик, Михал (2020). «Недостаток допустимого свойства дизъюнкции для разрешения k -ДНФ и NP-трудность его автоматизации». ЕССС . arXiv : 2003.10230 .

[BP-17] Бим, Пол ; Питасси, Тонианн (1996). «Упрощенные и улучшенные нижние границы разрешения». 37-й ежегодный симпозиум по основам информатики : 274–282.

[BW-18] Перейти обратно: Перейти обратно: ^а ^б Бен-Сассон, Эли ; Вигдерсон, Ави (1999). «Краткие доказательства узки - решение упрощено». Материалы 31-го симпозиума ACM по теории вычислений . стр. 517–526.

[cook-19] Кук, Стивен (1975). «Возможно конструктивные доказательства и исчисление предложений». Материалы 7-го ежегодного симпозиума ACM по теории вычислений . стр. 83–97.

[PW-20] Пэрис, Джефф ; Уилки, Алекс (1985). «Задачи подсчета в ограниченной арифметике». Методы математической логики . Конспект лекций по математике. Том. 1130. стр. 317–340. дои : 10.1007/BFb0075316 . ISBN 978-3-540-15236-1 .

[CN-21] Кук, Стивен ; Нгуен, Фуонг (2010). Логические основы сложности доказательства . Перспективы в логике. Кембридж: Издательство Кембриджского университета. дои : 10.1017/CBO9780511676277 . ISBN 978-0-521-51729-4 . МР 2589550 . ( проект 2008 года )

[Ajt-22] Аджтай, М. (1988). «Сложность принципа сортировки». Труды 29-го ежегодного симпозиума IEEE по основам компьютерных наук . стр. 346–355.

[Hak1-23] Хакен, А. (1985). «Неразрешимость разрешения». Теоретическая информатика . 39 : 297–308. дои : 10.1016/0304-3975(85)90144-6 .

[Ajtb-24] Аджтай, М. (1988). «Сложность принципа сортировки». Труды 29-го ежегодного симпозиума IEEE по основам компьютерных наук . стр. 346–355.

[KPW-25] Крайчек, Ян; Пудлак, Павел ; Вудс, Алан (1995). «Экспоненциальная нижняя граница размера ограниченной глубины. Доказательства Фреге принципа голубиной норы». Случайные структуры и алгоритмы . 7 (1): 15–39. дои : 10.1002/rsa.3240070103 .

[PBI-26] Питасси, Тонианн ; Бим, Пол ; Импальяццо, Рассел (1993). «Экспоненциальные нижние оценки принципа группировки». Вычислительная сложность . 3 (2): 97–308. дои : 10.1007/BF01200117 . S2CID 1046674 .

[Kr1-27] Крайчек, Ян (1994). «Нижние границы размера доказательств высказываний постоянной глубины». Журнал символической логики . 59 (1): 73–86. дои : 10.2307/2275250 . JSTOR 2275250 . S2CID 44670202 .

[Kr2-28] Перейти обратно: Перейти обратно: ^а ^б Крайчек, Ян (1997). «Интерполяционные теоремы, нижние оценки для систем доказательств и результаты о независимости для ограниченной арифметики». Журнал символической логики . 62 (2): 69–83. дои : 10.2307/2275541 . JSTOR 2275541 . S2CID 28517300 .

[Pu1-29] Перейти обратно: Перейти обратно: ^а ^б Пудлак, Павел (1997). «Нижние оценки разрешения, доказательства секущих плоскостей и монотонные вычисления». Журнал символической логики . 62 (3): 981–998. дои : 10.2307/2275583 . JSTOR 2275583 . S2CID 8450089 .

[PuNPpairs-30] Пудлак, Павел (2003). «О сводимости и симметрии непересекающихся NP-пар». Теоретическая информатика . 295 : 323–339. дои : 10.2307/2275583 . JSTOR 2275583 . S2CID 8450089 .

[KPb-31] Крайчек, Ян; Пудлак, Павел (1998). «Некоторые следствия криптографических гипотез для $S_{2}^{1}$ и EF» . Information and Computing . 140 (1): 82–94. doi : 10.1006/inco.1997.2674 .

[BPRb-32] Бонет, ML ; Питасси, Тонианн ; Раз, Ран (2000). «Об интерполяции и автоматизации системы доказательств Фреге». SIAM Journal по вычислительной технике . 29 (6): 1939–1967. дои : 10.1137/S0097539798353230 .

[BDGMPb-33] Бонет, ML ; Доминго, К.; Гавальда, Р.; Масиэль, А.; Питасси, Тонианн (2004). «Неавтоматизируемость доказательств Фреге ограниченной глубины». Вычислительная сложность . 13 (1–2): 47–68. дои : 10.1007/s00037-004-0183-5 . S2CID 1360759 .

[Hr1-34] Грубеш, Павел (2007). «Нижние границы модальной логики». Журнал символической логики . 72 (3): 941–958. дои : 10.2178/jsl/1191333849 . S2CID 1743011 .

[Hr2-35] Грубеш, Павел (2007). «Нижняя граница интуиционистской логики». Анналы чистой и прикладной логики . 146 (1): 72–90. дои : 10.1016/j.apal.2007.01.001 .

[Hr3-36] Грубеш, Павел (2009). «О длинах доказательств в неклассической логике» . Анналы чистой и прикладной логики . 157 (2–3): 194–205. дои : 10.1016/j.apal.2008.09.013 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]

[30]

[31]

[32]

[33]

[34]

[35]

[36]