Доказательство сжатия

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

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

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

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

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

${\displaystyle \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}$

Здесь мы видим:

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

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

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

Опровержение (резолюции) C — это доказательство резолюции из C. При наличии узла , это обычное отношение к предложению или 's, означающее предложение заключения , и (под)доказательство, означающее (под)доказательство, имеющее в качестве своего единственного корня.${\displaystyle \bot}$${\displaystyle \эта}$${\displaystyle \эта}$${\displaystyle \эта}$${\displaystyle \эта}$${\displaystyle \эта}$${\displaystyle \эта}$

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

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

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

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

Алгоритмы сжатия доказательств пропозициональной резолюции включают RecycleUnits , ^[2] RecyclePivots, ^[2] RecyclePivotsWithIntersection, ^[1] LowerUnits , ^[1] LowerUnivalents , ^[3] Split , ^[4] Reduce&Reconstruct , ^[5] и Subsumption.