RecycleUnits

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

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

1 функция RecycleUnits(Доказательство ):${\displaystyle P}$2 Пусть будет множеством нелистовых узлов, представляющих единичные предложения${\displaystyle U}$3 за каждое действие${\displaystyle u\in U}$ 4 Отметьте предков u5 для каждого неотмеченного do
6 пусть будет опорной переменной
7 пусть будет литералом, содержащимся в предложении
8 если то
9 замените левого родителя на
10 иначе если то
11 замените правого родителя на${\displaystyle n\in P}$ ${\displaystyle p}$${\displaystyle n}$${\displaystyle л}$${\displaystyle u}$ ${\displaystyle p==l}$ ${\displaystyle n}$${\displaystyle u}$ ${\displaystyle \neg p==l}$ ${\displaystyle n}$${\displaystyle u}$

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

1 функция ReconstructProof(Node ):${\displaystyle n}$3 если посещено вернуть
4 отметить как посещенное${\displaystyle n}$${\displaystyle n}$5 если нет родителей вернуть
6 иначе если есть только один родитель , то
7 ReconstructProof( )${\displaystyle n}$ ${\displaystyle n}$${\displaystyle x}$ ${\displaystyle x}$8 .Пункт = .Пункт${\displaystyle n}$${\displaystyle x}$9 else
10 пусть будет левым и правым родительским узлом${\displaystyle л}$${\displaystyle r}$11 пусть будет опорной переменной, используемой для вычисления
12 ReconstructProof( )${\displaystyle p}$${\displaystyle n}$${\displaystyle л}$13 РеконструкцияДоказательство( )${\displaystyle r}$14 если и
15 .Предложение = Resolve( , , )${\displaystyle p\in l.Предложение}$${\displaystyle p\in r.Пункт}$${\displaystyle n}$${\displaystyle л}$${\displaystyle r}$${\displaystyle p}$16 иначе если и
17 .Предложение = .Предложение${\displaystyle p\in l.Предложение}$${\displaystyle p\notin r.Пункт}$${\displaystyle n}$${\displaystyle r}$18 удалить ссылку на
19 else if и
20 .Clause = .Clause${\displaystyle л}$ ${\displaystyle p\in r.Пункт}$${\displaystyle p\notin l.Clause}$${\displaystyle n}$${\displaystyle л}$21 удалить ссылку на
22 иначе
23 пусть и //выбрать x эвристически${\displaystyle r}$${\displaystyle x\in \{l,r\}}$${\displaystyle y\in \{l,r\}\setminus \{x\}}$24 .Пункт = .Пункт${\displaystyle n}$${\displaystyle x}$25 удалить ссылку на${\displaystyle у}$

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

${\displaystyle (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 {красный}C_{8}(-1)}}}{C_{9}(3,5)}}}$

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

${\displaystyle (1){\cfrac {(2){\cfrac {{\color {красный}(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 содержится в правом родителе этого узла, и поэтому этот родитель заменяется на . Строка обозначает ссылку на предложение (структура теперь представляет собой направленный ациклический граф, а не дерево).${\displaystyle C_{8}}$${\displaystyle {C_{8}}^{*}}$${\displaystyle C_{8}}$

${\displaystyle (1){\cfrac {(2){\cfrac {(1){\cfrac {C_{1}(1,3)\qquad {\color {красный}{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)}}}$

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

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

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

${\displaystyle (1){\cfrac {{\cfrac {(1){\cfrac {C_{1}(1,3)\qquad {C_{8}}^{*}}{C_{3}(3)}}}{C_{7}{\color {красный}(3)}}}\qquad (4){\cfrac {C_{5}(-1,4)\qquad C_{6}(-1,-4)}{C_{8}(-1)}}}{C_{9}(3,5)}}}$

Снова левый родительский элемент не содержит опорную переменную, и выполняется та же операция, что и раньше.${\displaystyle C_{9}}$

${\displaystyle {\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 {красный}(3)}}}}$

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