RecycleUnits

В математической логике сжатие доказательств с помощью RecycleUnits метод сжатия пропозициональной логики доказательств разрешения . Его основная идея состоит в том, чтобы использовать промежуточные (например, невходящие) результаты доказательства, представляющие собой единичные предложения , то есть предложения, содержащие только один литерал. Определенные узлы доказательства можно заменить узлами, представляющими эти единичные предложения. После этой операции полученный граф преобразуется в валидное доказательство. Выходное доказательство короче оригинала, но при этом эквивалентно или сильнее.

Алгоритмы

Алгоритмы рассматривают доказательства разрешения как ориентированные ациклические графы , где каждый узел помечен предложением и каждый узел имеет одного или двух предшественников, называемых родительскими. Если у узла есть два родителя, он также помечается пропозициональной переменной, называемой опорной точкой, которая использовалась для вычисления предложения узлов с использованием разрешения.
Следующий алгоритм описывает замену узлов.
Предполагается, что при доказательстве разрешения для всех нелистовых узлов с двумя родительскими узлами левый родительский узел содержит положительную, а правый родительский узел — отрицательную переменную поворота. Алгоритм сначала перебирает все нелистовые элементы доказательства, а затем все непредшественные узлы доказательства. Если опорным элементом узла является переменная литерала текущего предложения unit, один из родительских узлов может быть заменен узлом, соответствующим этому предложению unit. Из-за вышеизложенного предположения, если литерал равен опорной точке, левый родительский элемент содержит литерал и может быть заменен узлом предложения единицы. Если литерал равен отрицанию опорной точки, правый родительский элемент заменяется.

1  function RecycleUnits(Proof $P$):
2      Let $U$ be the set of non leaf nodes representing unit clauses
3      for each $u\in U$ do
4          Mark the ancestors of u
5          for each unmarked $n\in P$ do
6              let $p$ be the pivot variable of $n$
7              let $l$ be the literal contained in the clause of $u$
8              if $p==l$ then
9                  replace the left parent of $n$ with $u$
10             else if $\neg p==l$ then
11                 replace the right parent of $n$ with $u$

В общем, после выполнения этой функции доказательство перестанет быть юридическим доказательством. Следующий алгоритм берет корневой узел доказательства и строит из него законное доказательство. Вычисления начинаются с рекурсивного вызова дочерних узлов. Чтобы минимизировать количество вызовов алгоритма, отслеживается, какие узлы уже были посещены. Обратите внимание, что доказательство разрешения можно рассматривать как общий ориентированный ациклический граф, а не как дерево. После рекурсивного вызова предложение текущего узла обновляется. При этом могут произойти четыре различных случая. Текущая переменная поворота может встречаться в обоих, левом, правом или ни в одном из родительских узлов. Если это происходит в обоих родительских узлах, предложение рассчитывается как резольвент родительских предложений. Если его нет ни в одном из родительских узлов, предложение этого родителя можно скопировать. Если он отсутствует у обоих родителей, приходится выбирать эвристически.

1  function ReconstructProof(Node $n$):
3      if $n$ is visited return
4      mark $n$ as visited
5      if $n$ has no parents return
6      else if $n$ has only one parent $x$ then
7          ReconstructProof($x$)
8          $n$.Clause = $x$.Clause
9      else
10         let $l$ be the left and $r$ the right parent node
11         let $p$ be the pivot variable used to compute $n$
12         ReconstructProof($l$)
13         ReconstructProof($r$)
14         if $p\in l.Clause$ and $p\in r.Clause$
15             $n$.Clause = Resolve($l$,$r$,$p$)
16         else if $p\in l.Clause$ and $p\notin r.Clause$
17             $n$.Clause = $r$.Clause
18             delete reference to $l$
19         else if $p\in r.Clause$ and $p\notin l.Clause$
20             $n$.Clause = $l$.Clause
21             delete reference to $r$
22         else
23             let $x\in \{l,r\}$ and $y\in \{l,r\}\setminus \{x\}$ //choose x heuristically
24             $n$.Clause = $x$.Clause
25             delete reference to $y$

Пример

Рассмотрим следующее доказательство резолюции.
Один промежуточный результат $C_{8}$ который представляет собой предложение единицы измерения (-1).

$(1){\cfrac {(2){\cfrac {(1){\cfrac {C_{1}(1,3)\qquad C_{2}(-1,2,5)}{C_{3}(2,3,5)}}\qquad C_{4}(1,-2)}{C_{7}(1,3,5)}}\qquad (4){\cfrac {C_{5}(-1,4)\qquad C_{6}(-1,-4)}{\color {red}C_{8}(-1)}}}{C_{9}(3,5)}}$

Существует один узел, не являющийся предком, использующий переменную 1 в качестве ведущего элемента: $C_{3}$.

$(1){\cfrac {(2){\cfrac {{\color {red}(1)}{\cfrac {C_{1}(1,3)\qquad C_{2}(-1,2,5)}{C_{3}(2,3,5)}}\qquad C_{4}(1,-2)}{C_{7}(1,3,5)}}\qquad (4){\cfrac {C_{5}(-1,4)\qquad C_{6}(-1,-4)}{C_{8}(-1)}}}{C_{9}(3,5)}}$

Литерал -1 содержится в правом родительском элементе этого узла, поэтому этот родительский элемент заменяется на $C_{8}$. Строка ${C_{8}}^{*}$ обозначает ссылку на пункт $C_{8}$ (структура теперь представляет собой ориентированный ациклический граф, а не дерево).

$(1){\cfrac {(2){\cfrac {(1){\cfrac {C_{1}(1,3)\qquad {\color {red}{C_{8}}^{*}}}{C_{3}(2,3,5)}}\qquad C_{4}(1,-2)}{C_{7}(1,3,5)}}\qquad (4){\cfrac {C_{5}(-1,4)\qquad C_{6}(-1,-4)}{C_{8}(-1)}}}{C_{9}(3,5)}}$

Эта структура больше не является юридическим доказательством, поскольку $C_{3}$ не является резольвентой $C_{1}$ и $C_{8}$. Поэтому его необходимо снова превратить в одно.
Первый шаг — обновить $C_{3}$. Поскольку сводная переменная 1 появляется в обоих родительских узлах, $C_{3}$ вычисляется как их резольвента.

$(1){\cfrac {(2){\cfrac {(1){\cfrac {C_{1}(1,3)\qquad {C_{8}}^{*}}{C_{3}{\color {red}(3)}}}\qquad C_{4}(1,-2)}{C_{7}(1,3,5)}}\qquad (4){\cfrac {C_{5}(-1,4)\qquad C_{6}(-1,-4)}{C_{8}(-1)}}}{C_{9}(3,5)}}$

Левый родительский узел $C_{7}$ не содержит сводную переменную, поэтому предложение этого родителя копируется в предложение $C_{7}$. Связь между $C_{7}$ и $C_{4}$ удален, и поскольку других ссылок на $C_{4}$ этот узел можно удалить.

$(1){\cfrac {{\cfrac {(1){\cfrac {C_{1}(1,3)\qquad {C_{8}}^{*}}{C_{3}(3)}}}{C_{7}{\color {red}(3)}}}\qquad (4){\cfrac {C_{5}(-1,4)\qquad C_{6}(-1,-4)}{C_{8}(-1)}}}{C_{9}(3,5)}}$

Опять левый родитель $C_{9}$ не содержит сводной переменной, и выполняется та же операция, что и раньше.

${\cfrac {\cfrac {(1){\cfrac {C_{1}(1,3)\qquad (4){\cfrac {C_{5}(-1,4)\qquad C_{6}(-1,-4)}{C_{8}(-1)}}}{C_{3}(3)}}}{C_{7}(3)}}{C_{9}{\color {red}(3)}}}$

Примечание: ссылка ${C_{8}}^{*}$ был заменен фактическим узлом доказательства $C_{8}$.
Результатом этого доказательства является пункт (3), который является более сильным результатом, чем пункты (3,5) исходного доказательства.