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

В теории доказательств , области математической логики , сжатие доказательств — это проблема алгоритмического сжатия формальных доказательств . Разработанные алгоритмы могут быть использованы для улучшения доказательств, генерируемых автоматизированными инструментами доказательства теорем , такими как решатели SAT , SMT-солверы , средства доказательства теорем первого порядка и помощники по доказательству .

Представление проблемы

В пропозициональной логике резолюция доказательства предложения $\kappa$ из набора предложений C представляет собой ориентированный ациклический граф (DAG): входные узлы представляют собой выводы аксиом (без посылок), выводы которых являются элементами C , резольвентные узлы являются выводами разрешения, а доказательство имеет узел с выводом $\kappa$.

DAG содержит ребро узла. $\eta _{1}$ к узлу $\eta _{2}$ тогда и только тогда, когда предпосылка $\eta _{1}$ является заключением $\eta _{2}$. В этом случае, $\eta _{1}$ является ребенком $\eta _{2}$, и $\eta _{2}$ является родителем $\eta _{1}$. Узел без дочерних элементов является корнем.

Алгоритм сжатия доказательств попытается создать новую группу DAG с меньшим количеством узлов, которая представляет собой действительное доказательство $\kappa$ или, в некоторых случаях, действительное доказательство подмножества $\kappa$.

Простой пример

Давайте возьмем доказательство разрешения для пункта $\left\{a,b,c\right\}$ из набора положений

$\left\{\eta _{1}:\left\{a,b,p\right\},\eta _{2}:\left\{c,\neg p\right\}\right\}\quad {\frac {\eta _{1}:a,b,p\quad \quad \eta _{2}:c,\neg p}{\eta _{3}:a,b,c}}p$

Здесь мы можем увидеть:

• $\eta _{1}$ и $\eta _{2}$ являются входными узлами.
• Узел $\eta _{3}$ имеет стержень $p$,
  • оставил разрешенный литерал $p$
  • правильно решенный литерал $\neg p$
• $\eta _{3}$ вывод - это пункт $\left\{a,b,c\right\}$
• $\eta _{3}$ помещения - вывод узлов $\eta _{1}$ и $\eta _{2}$ (его родители)
• DAG будет

${\begin{array}{ccc}\eta _{1}&&\eta _{2}\\&\nwarrow \nearrow \\&\eta _{3}\end{array}}$

• $\eta _{1}$ и $\eta _{2}$ являются родителями $\eta _{3}$
• $\eta _{3}$ является ребенком $\eta _{1}$ и $\eta _{2}$
• $\eta _{3}$ является корнем доказательства

(Резолюционное) опровержение C является резолюционным доказательством $\bot$ из С. ​Это общий узел $\eta$, ссылка на пункт $\eta$ или $\eta$Предложение 's, означающее заключительное положение $\eta$и (под)доказательство $\eta$ что означает (под)доказательство, имеющее $\eta$ как его единственный корень.

В некоторых работах можно найти алгебраическое представление резолюционного вывода . Резольвента $\kappa _{1}$ и $\kappa _{2}$ с шарниром $p$ можно обозначить как $\kappa _{1}\odot _{p}\kappa _{2}$. Когда опорная точка определена однозначно или не имеет значения, мы опускаем ее и пишем просто $\kappa _{1}\odot \kappa _{2}$. Таким образом, набор предложений можно рассматривать как алгебру с коммутативным оператором; а термины в соответствующей алгебре терминов обозначают доказательства резолюции в стиле обозначений, который более компактен и более удобен для описания доказательств резолюции, чем обычная запись в виде графа.

В нашем последнем примере обозначение DAG будет таким: $\left\{a,b,p\right\}\odot _{p}\left\{c,\neg p\right\}$ или просто $\left\{a,b,p\right\}\odot \left\{c,\neg p\right\}.$

Мы можем идентифицировать $\underbrace {\overbrace {\left\{a,b,p\right\}} ^{\eta _{1}}\odot \overbrace {\left\{c,\neg p\right\}} ^{\eta _{2}}} _{\eta _{3}}$.

Алгоритмы сжатия

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

Алгоритмы сжатия доказательств разрешения высказываний включают: RecycleUnits , RecyclePivots , RecyclePivotsWithIntersection , Нижние единицы , НижниеУниваленты , Расколоть , Уменьшить и реконструировать , и подчинение .