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

Введение

В логике и теоретической информатике, и в частности в теории доказательств и теории вычислительной сложности, сложность доказательств – это область, направленная на понимание и анализ вычислительных ресурсов, необходимых для доказательства или опровержения утверждений. Исследования в области сложности доказательств в основном сосредоточены на установлении нижних и верхних границ длины доказательств в различных системах доказательств. Например, одной из основных задач сложности доказательств является доказательство того, что система Фреге, стандартный пропозициональный исчисление, не допускает доказательства полиномиального размера для всех тавтологий. Здесь размер доказательства – это просто количество символов в нём, и доказательство считается полиномиальным, если его размер полиномиально зависит от размера доказываемой тавтологии. Систематическое изучение сложности доказательств началось с работы Стивена Кука и Роберта Рекхоу (1979), которые дали основное определение пропозициональной системы доказательств с точки зрения вычислительной сложности. В частности, Кук и Рекхоу отметили, что доказательство нижних границ размера доказательств для всё более мощных пропозициональных систем доказательств можно рассматривать как шаг к разделению NP и coNP (и, следовательно, P и NP), поскольку существование пропозициональной системы доказательств, допускающей доказательства полиномиального размера для всех тавтологий, эквивалентно NP = coNP. Современные исследования в области сложности доказательств используют идеи и методы из многих областей вычислительной сложности, алгоритмов и математики. Поскольку многие важные алгоритмы и алгоритмические методы можно представить как алгоритмы поиска доказательств для определенных систем доказательств, доказательство нижних границ на размеры доказательств в этих системах влечёт за собой нижние границы времени работы соответствующих алгоритмов. Это связывает сложность доказательств с более прикладными областями, такими как решение задачи SAT. Математическая логика также может служить основой для изучения размеров доказательств. Теории первого порядка и, в частности, слабые фрагменты арифметики Пеано, известные как ограниченная арифметика, служат унифицированными версиями пропозициональных систем доказательств и предоставляют дополнительную основу для интерпретации коротких пропозициональных доказательств с точки зрения различных уровней осуществимого рассуждения.

In logic and theoretical computer science, and specifically proof theory and computational complexity theory, proof complexity is the field aiming to understand and analyse the computational resources that are required to prove or refute statements. Research in proof complexity is predominantly concerned with proving proof length lower and upper bounds in various propositional proof systems. For example, among the major challenges of proof complexity is showing that the Frege system, the usual propositional calculus, does not admit polynomial size proofs of all tautologies. Here the size of the proof is simply the number of symbols in it, and a proof is said to be of polynomial size if it is polynomial in the size of the tautology it proves. Systematic study of proof complexity began with the work of Stephen Cook and Robert Reckhow (1979) who provided the basic definition of a propositional proof system from the perspective of computational complexity. Specifically Cook and Reckhow observed that proving proof size lower bounds on stronger and stronger propositional proof systems can be viewed as a step towards separating NP from coNP (and thus P from NP), since the existence of a propositional proof system that admits polynomial size proofs for all tautologies is equivalent to NP=coNP. Contemporary proof complexity research draws ideas and methods from many areas in computational complexity, algorithms and mathematics. Since many important algorithms and algorithmic techniques can be cast as proof search algorithms for certain proof systems, proving lower bounds on proof sizes in these systems implies run time lower bounds on the corresponding algorithms. This connects proof complexity to more applied areas such as SAT solving. Mathematical logic can also serve as a framework to study propositional proof sizes. First order theories and, in particular, weak fragments of Peano arithmetic, which come under the name of bounded arithmetic, serve as uniform versions of propositional proof systems and provide further background for interpreting short propositional proofs in terms of various levels of feasible reasoning.

Системы проверки

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

Ограниченная арифметика

Системы доказательств предложений могут быть интерпретированы как неравномерные эквиваленты теорий высшего порядка. Эквивалентность чаще всего изучается в контексте теорий ограниченной арифметики. Например, система расширенной Фреге соответствует теории Кука, формализующей рассуждения за полиномиальное время, а система Фреге соответствует теории, формализующей рассуждения. Это соответствие было введено Стивеном Куком (1975), который показал, что теоремы coNP, формально – формулы теории, переводятся в последовательности тавтологий с доказательствами полиномиального размера в системе расширенной Фреге. Более того, расширенная Фреге является самой слабой системой с таким свойством: если другая система доказательств P обладает этим свойством, то P имитирует расширенную Фреге. Альтернативный перевод между утверждениями второго порядка и формулами предложений, предложенный Джеффом Парисом и Алексом Уилки (1985), оказался более практичным для описания подсистем расширенной Фреге, таких как Фреге или Фреге с постоянной глубиной. В то время как вышеупомянутое соответствие утверждает, что доказательства в теории переводятся в последовательности коротких доказательств в соответствующей системе доказательств, справедлива и обратная импликация. Можно получить нижние оценки на размер доказательств в системе доказательств P, построив подходящие модели теории T, соответствующей системе P. Это позволяет доказывать нижние оценки сложности с помощью конструкций в теории моделей, подход, известный как метод Аджая.

Решающие задачи SAT

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

Нижняя граница

Доказать нижние оценки длины доказательств пропозициональных формул, как правило, очень сложно. Тем не менее, было обнаружено несколько методов для доказательства нижних оценок для слабых систем доказательств. Хакен (1985) доказал экспоненциальную нижнюю оценку для метода резолюций и принципа Дирихле. Аджтай (1988) доказал суперополиномиальную нижнюю оценку для системы Фреге с постоянной глубиной и принципа Дирихле. Эта оценка была усилена до экспоненциальной Кражичеком, Пудлаком и Вудсом, а также Питасси, Бимом и Импаглиаццо. В доказательстве Аджтая используется метод случайных ограничений, который также применялся для получения нижних оценок сложности цепей для AC0. Кражичек (1994) сформулировал метод осуществимой интерполяции и впоследствии использовал его для получения новых нижних оценок для метода резолюций и других систем доказательств. Пудлак (1997) доказал экспоненциальные нижние оценки для метода секущих плоскостей с помощью осуществимой интерполяции. Бен-Сассон и Вигдерсон (1999) предложили метод доказательства, сводящий нижние оценки размера опровержений методом резолюций к нижним оценкам ширины опровержений методом резолюций, что охватывает многие обобщения нижней оценки Хакена. Вывод нетривиальной нижней оценки для системы Фреге остаётся давней открытой проблемой.

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

Рассматриваем тавтологию вида. Тавтология истинна для любого выбора , и после фиксации оценки и независимы, поскольку они определены на непересекающихся множествах переменных. Это означает, что можно определить интерполянтную схему , такую что выполняются оба условия и . Интерполянтная схема определяет, является ли ложным или истинным, рассматривая только. Структура интерполянтной схемы может быть произвольной. Тем не менее, доказательство исходной тавтологии можно использовать в качестве подсказки о том, как построить . Система доказательств P считается обладающей осуществимой интерполяцией, если интерполянт эффективно вычисляется из любого доказательства тавтологии в P. Эффективность измеряется относительно длины доказательства: интерполянты для более длинных доказательств вычислить проще, поэтому это свойство представляется антимонотонным по отношению к силе системы доказательств. Следующие три утверждения не могут быть одновременно верными: (a) имеет короткое доказательство в некоторой системе доказательств; (b) эта система доказательств обладает осуществимой интерполяцией; (c) интерполянтная схема решает вычислительно сложную задачу. Очевидно, что (a) и (b) подразумевают существование небольшой интерполянтной схемы, что противоречит (c). Эта взаимосвязь позволяет преобразовывать верхние оценки длины доказательства в нижние оценки сложности вычислений и, наоборот, эффективные алгоритмы интерполяции – в нижние оценки длины доказательства. Некоторые системы доказательств, такие как метод резолюций и метод секущих плоскостей, допускают осуществимую интерполяцию или ее варианты. Осуществимая интерполяция может рассматриваться как слабая форма автоматизируемости. Фактически, для многих систем доказательств, таких как Extended Frege, осуществимая интерполяция эквивалентна слабой автоматизируемости. В частности, многие системы доказательств P способны доказать свою собственную корректность, что является тавтологией, утверждающей, что "если является P-доказательством формулы , то выполняется". Здесь кодируются свободными переменными. Более того, P-доказательства можно генерировать в полиномиальное время, учитывая длину , и, следовательно, эффективный интерполянт, полученный из коротких P-доказательств корректности P, будет определять, допускает ли данная формула короткое P-доказательство. Такой интерполянт можно использовать для определения системы доказательств R, свидетельствующей о слабой автоматизируемости P. С другой стороны, слабая автоматизируемость системы доказательств P подразумевает, что P допускает осуществимую интерполяцию. Однако, если система P не доказывает эффективно свою собственную корректность, то она может быть не слабо автоматизируемой, даже если допускает осуществимую интерполяцию. Многие результаты, связанные с неотоматизируемостью, предоставляют аргументы против осуществимой интерполяции в соответствующих системах. Krajíček и Pudlák (1998) доказали, что Extended Frege не допускает осуществимой интерполяции, если RSA не является безопасной относительно P/poly. Bonet, Pitassi и Raz (2000) доказали, что система Frege не допускает осуществимой интерполяции, если схема Диффи — Хеллмана не является безопасной относительно P/poly. Bonet, Domingo, Gavaldá, Maciel, Pitassi (2004) доказали, что системы Frege постоянной глубины не допускают осуществимой интерполяции, если схема Диффи — Хеллмана не является безопасной против неuniformных противников, работающих в субекспоненциальное время.

Consider a tautology of the form The tautology is true for every choice of , and after fixing the evaluation of and are independent because they are defined on disjoint sets of variables. This means that it is possible to define an interpolant circuit , such that both and hold. The interpolant circuit decides either if is false or if is true, by only considering The nature of the interpolant circuit can be arbitrary. Nevertheless, it is possible to use a proof of the initial tautology as a hint on how to construct A proof systems P is said to have feasible interpolation if the interpolant is efficiently computable from any proof of the tautology in P. The efficiency is measured with respect to the length of the proof: it is easier to compute interpolants for longer proofs, so this property seems to be anti monotone in the strength of the proof system. The following three statements cannot be simultaneously true: (a) has a short proof in a some proof system; (b) such proof system has feasible interpolation; (c) the interpolant circuit solves a computationally hard problem. It is clear that (a) and (b) imply that there is a small interpolant circuit, which is in contradiction with (c). Such relation allows the conversion of proof length upper bounds into lower bounds on computations, and dually to turn efficient interpolation algorithms into lower bounds on proof length. Some proof systems such as Resolution and Cutting Planes admit feasible interpolation or its variants. Feasible interpolation can be seen as a weak form of automatability. In fact, for many proof systems, such as Extended Frege, feasible interpolation is equivalent to weak automatability. Specifically, many proof systems P are able to prove their own soundness, which is a tautology stating that `if is a P proof of a formula then holds'. Here, are encoded by free variables. Moreover, it is possible to generate P proofs of in polynomial time given the length of and Therefore, an efficient interpolant resulting from short P proofs of soundness of P would decide whether a given formula admits a short P proof Such an interpolant can be used to define a proof system R witnessing that P is weakly automatable. On the other hand, weak automatability of a proof system P implies that P admits feasible interpolation. However, if a proof system P does not prove efficiently its own soundness, then it might not be weakly automatable even if it admits feasible interpolation. Many non automatability results provide evidence against feasible interpolation in the respective systems. Krajíček and Pudlák (1998) proved that Extended Frege does not admit feasible interpolation unless RSA is not secure against P/poly. Bonet, Pitassi and Raz (2000) proved that the Frege system does not admit feasible interpolation unless the Diffie–Helman scheme is not secure against P/poly. Bonet, Domingo, Gavaldá, Maciel, Pitassi (2004) proved that constant depth Frege systems of do not admit feasible interpolation unless the Diffie–Helman scheme is not secure against nonuniform adversaries working in subexponential time.

Неклассическая логика

Идея сравнения размера доказательств применима к любой процедуре автоматизированного вывода, генерирующей доказательство. Некоторые исследования посвящены размеру доказательств в пропозициональных неклассических логиках, в частности, интуиционистской, модальной и немонотонной логиках. Хрубеш (2007–2009) доказал экспоненциальные нижние оценки размера доказательств в системе расширенной Фреге для некоторых модальных и интуиционистской логик, используя вариант монотонной реализуемой интерполяции.