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

9

Я пытаюсь понять статью о p-оптимальных системах доказательства и логике для PTIME . В статье есть понятие, называемое системами доказательства, и я не понимаю интуиции:

Σ={0,1} ... Мы выявляем проблемы с подмножествами Q в Σ,

Я думаю, что интуиция заключается в том, что мы кодируем определенную структуру в Σ (например, неориентированные графы) и подмножества этих структур являются проблемами (например, плоские графы).

Система доказательств для проблемыQΣ сюръективная функция P:ΣQ вычислимо за полиномиальное время.

Теперь можно сказать, Σэто множество всех возможных моделей в определенной структуре (например, все неориентированные графы). Но это не имеет смысла, потому что почему неориентированные графы должны отображаться на подмножестве? Это могут быть закодированы машины Тьюринга, но это тоже не имеет смысла ...

Любые идеи?

Иоахим
источник

Ответы:

8

Думать о Σ кодирование каких-то объектов, и Qкак совокупность всех объектов, удовлетворяющих некоторому свойству. Думать оP как функция, которая принимает (кодирование) пары (x,p) где x это объект и p якобы "доказательство" xQ, ФункцияP является «проверкой проверки»: она проверяет, что p на самом деле представляет собой достоверное доказательство того, что xQ, Если так, то возвращаетсяxв противном случае он возвращает элемент по умолчанию Q,

В качестве примера предположим, Σ кодирует графики и позволяет Qбыть множеством (кодировок) гамильтоновых графов. ВозможноP это: декодировать ввод как (G,) где G это график и список вершин G; подтвердите это гамильтонов цикл G; если так то вернисьG в противном случае верните график в одну точку.

Вы рассмотрели случай плоских графов. Чтобы получить подходящийP нам нужно понятие поли-проверяемого времени доказательства плоскостности.

В общем вход на P не нужно кодировать пару (x,p), Важно то, чтоP может извлечь две части информации из своего ввода: рассматриваемый объект и предполагаемые доказательства того, что объект принадлежит Q, Например, давайте возьмем в качествеQмножество всех предложений, доказуемых в некоторой теории первого порядка. Сейчас жеPдекодирует свой ввод как формальное доказательство. Если кодировка неверна, возвращается, Если кодировка представляет действительное доказательство, оно возвращает утверждение, которое было подтверждено доказательством (которое, вероятно, является корнем дерева доказательств или последней формулой в последовательности утверждений, в зависимости от того, как вы формализуете доказательства).

Андрей Бауэр
источник
5

Вы должны подумать о вводе системы доказательства P как текст доказательства π элемента qQ, Если текст действителен, чтоP(π)=q, в противном случае P(π) некоторые исправлены q0Q, Мы хотимP быть polytime, поскольку это означает, что доказательство легко проверить.

В качестве примера предположим, Q набор пропозициональных тавтологий, и Pлюбая система доказательства в гильбертовом стиле, которая состоит из набора линий , каждая из которых является аксиомой или следует из предыдущих строк с помощью правила деривации (обычно Modus Ponens). Если доказательство действительно, тоPдолжен вывести последнюю строку в доказательстве. В противном случае выведите некоторую фиксированную тавтологию, такую ​​какp¬p,

Вернемся к первому вопросу, Qявляется кодировкой всех структур определенного типа, удовлетворяющих некоторому свойству. Одним из примеров является тавтология. Другим примером является множество всех не раскрашиваемых графов, которые имеют систему доказательств, известную как исчисление Хайоса.

Юваль Фильмус
источник