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

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

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

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

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

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

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

Примеры пропозициональных систем доказательства включают в себя последовательное исчисление , разрешение , плоскости отсечения и систему Фреге . Сильные математические теории, такие как ZFC, также порождают системы пропозициональных доказательств: доказательство тавтологии в пропозициональной интерпретации ZFC - это ZFC-доказательство формализованного утверждения « является тавтологией». ${\ Displaystyle \ тау}$ ${\ Displaystyle \ тау}$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Хакен (1985) доказал экспоненциальную нижнюю границу для разрешения и принципа ячейки. ^[22]
Ajtai (1988) доказал суперполиномиальную нижнюю границу для системы Фреге постоянной глубины и принципа голубятни. ^[21] Это было усилено до экспоненциальной нижней границы Крайичеком, Пудлаком и Вудсом ^[23], а также Питасси, Бимом и Импальяццо. ^[24] Нижняя граница Аджтаи использует метод случайных ограничений, который также использовался для получения нижних оценок AC 0 сложности схемы .
Krajíček (1994) ^[25] сформулировал метод допустимой интерполяции и позже использовал его для получения новых нижних оценок для Резолюции и других систем доказательства. ^[26]
Пудлак (1997) доказал экспоненциальные нижние оценки для секущих плоскостей с помощью допустимой интерполяции. ^[27]
Бен-Сассон и Вигдерсон (1999) представили метод доказательства, снижающий нижние границы размера опровержений Резолюции до нижних границ ширины опровержений Резолюции, который захватил многие обобщения нижней границы Хакена. ^[17]

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

Возможная интерполяция [ править ]

Рассмотрим тавтологию формы . Тавтология верна для любого выбора и после фиксации оценки и являются независимыми, потому что они определены на непересекающихся наборах переменных. Это означает, что можно определить схему интерполяции , в которой выполняются оба и . Схема интерполянта решает, является ли оно ложным или истинным, только путем рассмотрения . Характер схемы интерполянта может быть произвольным. Тем не менее, можно использовать доказательство исходной тавтологии как подсказку о том, как строить . Говорят, что система доказательств P имеет допустимую интерполяцию. ${\ Displaystyle А (х, у) \ вправо В (у, г)}$ $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)$

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

Некоторые системы проверки, такие как Разрешение и Плоскости сечения, допускают допустимую интерполяцию или ее варианты. ^[26]^[27]

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

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

Krajíček и Pudlák (1998) доказали, что Extended Frege не допускает выполнимой интерполяции, если RSA не защищен от P / poly. ^[7]
Бонет, Питасси и Раз (2000) доказали, что система -Frege не допускает допустимой интерполяции, если схема Диффи-Хелмана не защищена от P / poly. ^[6] $TC^{0}$
Bonet, Domingo, Gavaldá, Maciel, Pitassi (2004) доказали, что системы Фреге с постоянной глубиной не допускают допустимой интерполяции, если только схема Диффи-Хельмана не защищена от неоднородных противников, работающих в субэкспоненциальном времени. ^[8]

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

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

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

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

Вычислительная сложность
Сложность схемы
Коммуникационная сложность
Математическая логика
Теория доказательств
Классы сложности
НП (сложность)
coNP

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

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

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

Бим, Пол; Pitassi, Toniann (1998), "Пропозициональное доказательство сложности: прошлое, настоящее и будущее", Бюллетень Европейской ассоциации по теоретической информатике , 65 : 66-89, MR 1650939 , ECCC TR98-067
Повар, Стивен ; Нгуен, Фуонг (2010), Логические основы сложности доказательства , перспективы в логике, Кембридж: Cambridge University Press, 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), «Длина доказательств», в Buss, SR (ed.), Handbook of Proof Theory , Studies in Logic and the Foundations of Mathematics, 137 , Amsterdam: North-Holland, pp. 547–637 , DOI : 10.1016 / S0049-237X (98) 80023-2 , MR 1640332

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

Доказательство сложности
Список рассылки доказательств сложности.

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

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

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

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

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

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

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

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

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

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

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

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

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

[GKMP-14] Göös, Мика; Корот, Саджин; Мерц, Ян; Питасси, Тонниан (2020). «Автоматизировать раскройные рубки NP-сложно». STOC : 68–77. arXiv : 2004.08037 . DOI : 10.1145 / 3357713.3384248 . ISBN 9781450369794. S2CID 215814356 .

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

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

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

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

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

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

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

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

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

[PBI-24] Pitassi, Toniann ; Бим, Пол ; Impagliazzo, Рассел (1993). «Экспоненциальные нижние оценки для принципа ячейки». Вычислительная сложность . 3 (2): 97–308. DOI : 10.1007 / BF01200117 . S2CID 1046674 .

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

[Kr2-26] Krajíček, Ян (1997). «Теоремы интерполяции, нижние оценки для систем доказательства и результаты о независимости для ограниченной арифметики». Журнал символической логики . 62 (2): 69–83. DOI : 10.2307 / 2275541 . JSTOR 2275541 .

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

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

[Hr1-29] Hrubeš, Павел (2007). «Нижние оценки модальных логик». Журнал символической логики . 72 (3): 941–958. DOI : 10.2178 / JSL / 1191333849 .

[Hr2-30] Hrubeš, Павел (2007). «Нижняя граница интуиционистской логики». Летопись чистой и прикладной логики . 146 (1): 72–90. DOI : 10.1016 / j.apal.2007.01.001 .

[Hr3-31] Hrubeš, Павел (2009). «О длинах доказательств в неклассических логиках». Летопись чистой и прикладной логики . 157 (2–3): 194–205. DOI : 10.1016 / j.apal.2008.09.013 .

[1]