NP против co-NP и логика второго порядка

11

Предположим, что NP = co-NP, а полином ограничивает длину доказательства неудовлетворенности для экземпляра 3-CNF x . Тогда есть ли какие-либо результаты о том, в какой форме может быть получено любое доказательство неудовлетворенности для x длины p ( x ) ? Т.е. в целом, должно ли такое доказательство использовать, например, всю мощь логики второго порядка над бесконечными структурами (я знаю, что предложение доказать - неудовлетворительная формула может быть выражено в логике второго порядка над конечные структуры, но промежуточные шаги в доказательстве, чтобы добраться до этого, могут потребовать рассуждений по бесконечным структурам)p(x)xxp(x)

Поскольку не существует эффективной, полной и надежной системы логического вывода для логики второго порядка, можно ли будет использовать такой результат для доказательства NP co-NP?

выбирать
источник
2
Связанный (но не точный дубликат): cstheory.stackexchange.com/questions/3064/…
Tsuyoshi Ito

Ответы:

7

Если существует оптимальная pps (pps = система пропозициональных доказательств , оптимальная pps - это pps, которая может p-симулировать любую другую систему доказательств), то pps EF (Extended Frege) усилена пропозициональными аксиомами, утверждающими обоснованность оптимальной системы пропозициональных доказательств. будет оптимальным. В более общем смысле EF + обоснованность pps P может p-моделировать P для любого P. Таким образом, EF имеет своего рода общность: вам не нужно менять логику или базовую структуру pps, а просто добавить аксиомы высказываний, чтобы получить любую произвольные сильные pps.

NP=coNP

πφφ

В целом, нет необходимости выходить за пределы логики высказываний.

NP=coNPNPcoNP

Кава
источник
1
Ответ у меня над головой, но арабский текст в нем вызвал у меня любопытство. :)
Tsuyoshi Ito
@Tsuyoshi: это был "the", набранный с использованием персидской клавиатуры. :)
Kaveh
Ой, извините за ошибку!
Цуёси Ито
Спасибо за ответ. Знаете ли вы ссылку на утверждение "NP = coNP эквивалентно существованию супер pps"? Благодаря!
Выберите
3
Это классический результат работы Cook-Reckhow 1979 года, но это не сложно. Pps - это средство проверки сертификата для TAUT, а TAUT - полный язык coNP. Если длины доказательств являются полиномиальными для некоторых pps, TAUT будет в NP. Для другого направления, если NP = coNP, то есть алгоритм NP для TAUT, сертификаты являются доказательствами, а верификатор - pps.
Каве