Пропозициональная система доказательства

В исчислении высказываний и сложности доказательства система доказательства высказываний ( pps ), также называемая системой доказательства высказываний Кука – Рекхоу , представляет собой систему для доказательства классических тавтологий высказываний .

Математическое определение

Формально pps — это с полиномиальным временем функция P которой , диапазон представляет собой набор всех пропозициональных тавтологий (обозначаемых TAUT). ^[1] Если A — формула, то любой x такой, что P ( x ) = A называется P -доказательством A. , Условие, определяющее pps, можно разбить следующим образом:

Полнота : каждая пропозициональная тавтология имеет P -доказательство.
Разумность : если пропозициональная формула имеет P -доказательство, то это тавтология.
Эффективность : P работает за полиномиальное время .

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

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

Если P ₁ является pps согласно первому определению, то P ₂ определяется посредством P ₂ ( A , x ) тогда и только тогда, когда P ₁ ( x ) = A является pps согласно второму определению. И наоборот, если P ₂ является pps согласно второму определению, то P ₁ определяется формулой

P_{1}(\langle x,A\rangle )={\begin{cases}A&{\text{if }}P_{2}(A,x)\\\top &{\text{otherwise}}\end{cases}}

( P ₁ принимает на вход пары) — это pps согласно первому определению, где $\top$ является фиксированной тавтологией.

Алгоритмическая интерпретация

Второе определение можно рассматривать как недетерминированный алгоритм определения принадлежности к TAUT. Это означает, что доказательство нижней границы суперполиномиального размера доказательства для pps исключит существование определенного класса алгоритмов с полиномиальным временем, основанных на этом pps.

Например, нижние границы экспоненциального размера доказательства разрешения для принципа «ячейки» подразумевают, что любой алгоритм, основанный на разрешении, не может эффективно определять TAUT или SAT и потерпит неудачу из-за тавтологии принципа «ячейки» . Это важно, поскольку класс алгоритмов, основанных на разрешении, включает большинство современных алгоритмов поиска доказательства высказываний и современных промышленных решателей SAT.

История

Исторически исчисление высказываний Фреге было первой системой доказательства высказываний. Общее определение системы пропозициональных доказательств принадлежит Стивену Куку и Роберту А. Рекхоу (1979). ^[1]

Связь с теорией сложности вычислений

Систему доказательства высказываний можно сравнить, используя понятие p-симуляции . Система пропозициональных доказательств P p-моделирует Q (записанный как P ≤ _p Q ), когда существует функция F с полиномиальным временем такая, что P ( F ( x )) = Q ( x ) для каждого x . ^[1] То есть, имея Q -доказательство x , мы можем за полиномиальное время найти P -доказательство той же тавтологии. Если P ⩽ _p Q и Q ⩽ _p P , системы доказательств P и Q эквивалентны p- . Существует также более слабое понятие моделирования: pps P имитирует или слабо p-моделирует pps Q , если существует полином p такой, что для каждого Q -доказательства x тавтологии A существует P -доказательство y для A такое, что что длина y , | й | не превосходит p (| x |). (Некоторые авторы используют слова «p-моделирование» и «симуляция» как синонимы для любого из этих двух понятий, обычно для последнего.)

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

Если P полиномиально ограничен и Q моделирует P , то Q также полиномиально ограничен.

Множество пропозициональных тавтологий TAUT представляет собой coNP -полный набор. Система пропозициональных доказательств — это сертификат-верификатор членства в TAUT. Существование полиномиально ограниченной системы пропозиционального доказательства означает, что существует верификатор с сертификатами полиномиального размера, т. е. TAUT находится в NP . На самом деле эти два утверждения эквивалентны, т. е. существует полиномиально ограниченная система пропозициональных доказательств тогда и только тогда, когда классы сложности NP и coNP равны. ^[1]

Некоторые классы эквивалентности систем доказательства при моделировании или p -моделировании тесно связаны с теориями ограниченной арифметики ; по сути, они являются «неоднородными» версиями ограниченной арифметики, точно так же, как классы схем являются неоднородными версиями классов сложности, основанной на ресурсах. «Расширенные системы Фреге» (позволяющие вводить новые переменные по определению) соответствуют, таким образом, например, полиномиально ограниченным системам. Там, где ограниченная арифметика, в свою очередь, соответствует классу сложности, основанному на схемах, часто существует сходство между теорией систем доказательства и теорией семейств схем, например сопоставление результатов нижних оценок и разделения. Например, так же, как счет не может производиться с помощью $\mathbf {AC} ^{0}$ Семейство схем субэкспоненциального размера, многие тавтологии, относящиеся к принципу группировки, не могут иметь субэкспоненциальные доказательства в системе доказательств, основанной на формулах ограниченной глубины (и, в частности, не в системах, основанных на разрешении, поскольку они полагаются исключительно на формулы глубины 1).

Примеры систем пропозициональных доказательств

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

Некоторые примеры изучаемых систем пропозициональных доказательств:

Пропозициональное разрешение и различные его ограничения и расширения, такие как алгоритм DPLL.
Естественный вычет
Секвенционное исчисление
Система Фреге
Расширенная система Фреге
Полиномиальное исчисление
Система нулевой установки
Метод секущей плоскости
Семантическая таблица

Ссылки

^ Jump up to: ^а ^б ^с ^д Кук, Стивен ; Рекхау, Роберт А. (1979). «Относительная эффективность систем доказательства высказываний». Журнал символической логики . Том. 44, нет. 1. С. 36–50. JSTOR 2273702 .

Дальнейшее чтение

Сэмюэл Басс (1998), «Введение в теорию доказательств», в: Справочник по теории доказательств (ред. SRBuss), Elsevier (1998).
П. Пудлак (1998), « Длина доказательств », в: Справочник по теории доказательств (ред. SRBuss), Elsevier, (1998).
П. Бим и Т. Питасси (1998). Сложность доказательства высказываний: прошлое, настоящее и будущее . Технический отчет TR98-067, Электронный коллоквиум по сложности вычислений.
Натан Сегерлинд (2007) «Сложность доказательств высказываний» , Бюллетень символической логики 13 (4): 417–481.
Дж. Крайчек (1995), Ограниченная арифметика, логика высказываний и теория сложности , издательство Кембриджского университета.
Я. Крайичек, Сложность доказательства , в: Proc. 4-й Европейский математический конгресс (под ред. А. Лаптева), EMS, Цюрих, стр. 221–231 (2005).
Александр А. Разборов, Сложность доказательства высказываний , в кн.: Тр. 8-й Европейский математический конгресс , EMS, Порторож, стр. 439–464 (2023).
Я. Крайичек, Сложность доказательства высказываний I. и Сложность доказательства и арифметика .
Стивен Кук и Фуонг Нгуен, Логические основы сложности доказательств , Cambridge University Press, 2010 ( проект 2008 г. )
Роберт Рекхоу, О длинах доказательств в исчислении высказываний , докторская диссертация, 1975.

Внешние ссылки

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

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

[1]