Теоретическое ограничение графа на доказательства в теории сложности доказательств

Доказательство сложности является основной областью теории вычислительной сложности. Конечная цель этой области состоит в том, чтобы доказать , то есть любой доказатель не может дать доказательство неудовлетворенности данной входной формулой. $NP\neq coNP$

Граф - это одна из формальных моделей доказательств. Мой вопрос о дальнейшем ограничении этой модели.

Доказательство представляется в виде DAG. Узлы с веером 0 имеют аксиомные метки. Уникальный узел с разветвлением 0 соответствует «ложь». Для заданных правил ввода вывода каждый узел, который имеет как степень, так и степень, имеет метку, представляющую предложение.

Мой вопрос:

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

Имеют ли те Доказательные Системы, которые ранее изучались, такие как Nullstellensatz, Resolution, LS, AC0 Frege, RES (k), Полиномиальное Исчисление и Плоскости, некоторую теоретическую характеристику графа ??

Наиболее естественным ограничением на доказательстве DAG является то, что оно должно быть деревом, то есть любая «лемма» (промежуточный вывод) не используется более одного раза. Это свойство называется «древовидным». Общее разрешение экспоненциально более мощное, чем древовидное, как показано, например, Бен-Сассоном, Импальяццо и Вигдерсоном . Эта концепция также была рассмотрена для других систем доказательств - просто найдите «древовидный X», где X - интересующая вас система доказательств. В конкретном случае разрешения существуют другие ограничения, которые могут быть рассмотрены. См., Например, статью Алехновича, Йоханнсена, Питасси и Уркхарта о регулярном разрешении.

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

Мюллер и Сзейдер изучают Резолюционные доказательства, где доказательство DAG имеет ограниченную ширину дерева или ограниченную ширину пути (для подходящих расширений этих мер сложности графов на ориентированные графы.)

Они показывают, что ширина пути DAG по существу равна пространственной сложности доказательства, и определяют обобщенное понятие пространства доказательства, которое эквивалентно ширине дерева.

Для достаточно сильных систем доказательств графическое представление доказательства в системе кажется менее последовательным, поскольку (как уже отмечал Джошуа Грохов) DAG-подобные и древовидные доказательства Фреге полиномиально эквивалентны (см. Монографию Крайчека за 1995 год для доказательства этого факта). ).

Для более слабых систем доказательств, таких как разрешение, древовидная структура экспоненциально слабее, чем у DAG-подобных доказательств (как описано выше у Yuval Filmus).

Бекман и Бусс [1] (следуя Бекману [2] ) рассмотрели ограничение высоты (эквивалентно глубине) графа доказательств с постоянной глубиной доказательств Фреге и исследовали связь между DAG-подобным, размером дерева и высотой постоянной глубины Доказательства Фреге. (Обратите внимание на различие между ограничением глубины графа проверки и ограничением глубины контура, появляющегося в линии доказательства).

Также могут существовать различия между древовидными и DAG-подобными доказательствами Nullstellensatz (и полиномиального исчисления), которые я в настоящее время не помню.