Нижние единицы

При сжатии доказательств LowerUnits ( LU ) — это алгоритм, используемый для сжатия доказательств разрешения логики высказываний . Основная идея LowerUnits заключается в использовании следующего факта:

Theorem: Let $\varphi$ be a potentially redundant proof, and $\eta$ be the redundant proof | redundant node. If $\eta$’s clause is a unit clause, 
then $\varphi$ is redundant.

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

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

Необходимо соблюдать осторожность в случаях, когда узел узла $\eta ^{\prime }$ встречается выше в дополнительном доказательстве, которое выводит еще один единичный узел $\eta$. В таких случаях $\eta$ зависит от $\eta ^{\prime }$. Позволять $\ell$ быть единственным литералом единичного предложения $\eta ^{\prime }$. Тогда любое появление ${\overline {\ell }}$ в поддоказательстве выше $\eta$ не будут отменены резолюцией выводов с $\eta ^{\prime }$ больше. Следовательно, ${\overline {\ell }}$ будет распространяться вниз, когда доказательство будет зафиксировано, и появится в пункте $\eta$. Трудностей с такими зависимостями можно легко избежать, если повторно вставить верхний единичный узел. $\eta ^{\prime }$ после повторной вставки единичного узла $\eta$ (т.е. после повторной установки, $\eta ^{\prime }$ должен появиться ниже $\eta$, чтобы отменить дополнительный литерал ${\overline {\ell }}$ от $\eta$пункт). Этого можно добиться, собирая единичные узлы в очередь во время обхода доказательства снизу вверх и повторно вставляя их в том порядке, в котором они были поставлены в очередь.

Алгоритм исправления доказательства, содержащего множество корней, выполняет обход доказательства сверху вниз, пересчитывает резольвенты и заменяет сломанные узлы (например, узлы, у которых удален NodeMarker в качестве одного из своих родителей) их выжившими родителями (например, другим родителем, в случае, если один из них удален). родительский элемент был удаленNodeMarker).

Когда единичные узлы собираются и удаляются из доказательства утверждения $\kappa$ и доказательство зафиксировано, пункт $\kappa ^{\prime }$ в корневом узле нового доказательства не равно $\kappa$ больше, но содержит (некоторые) двойственные литералы единичных предложений, которые были удалены из доказательства. Повторная вставка единичных узлов внизу доказательства решает проблему. $\kappa ^{\prime }$ с положениями (некоторых) собранных единичных узлов, чтобы получить доказательство $\kappa$ снова.

Алгоритм

Общая структура алгоритма

Algorithm LowerUnits
  Input: A proof $\psi$
  Output: A proof $\psi ^{\prime }$ with no global redundancy with unit redundant node

  (unitsQueue, $\psi _{b}$) ← collectUnits($\psi$); 
  $\psi _{f}$ ← fix($\psi _{b}$); 
  fixedUnitsQueue ← fix(unitsQueue); 
  $\psi ^{\prime }$ ← reinsertUnits($\psi _{f}$, fixedUnitsQueue);
  return $\psi ^{\prime }$;

• « ←» означает присвоение . Например, « самый большой ← элемент » означает, что значение самого большого изменяется на значение элемента .
• « return » завершает алгоритм и выводит следующее значение.

Мы собираем пункты блока следующим образом.

Algorithm CollectUnits
  Input: A proof $\psi$
  Output: A pair containing a queue of all unit nodes (unitsQueue) that are used more than once in $\psi$ and a broken proof $\psi _{b}$

$\psi _{b}$ ← $\psi$; 
traverse $\psi _{b}$ bottom-up and foreach node $\eta$ in $\psi _{b}$ do
  if $\eta$ is unit and $\eta$ has more than one child then
      add $\eta$ to unitsQueue; 
      remove $\eta$ from $\psi _{b}$; 
  end
end
return (unitsQueue, $\psi _{b}$); 

• « ←» означает присвоение . Например, « самый большой ← элемент » означает, что значение самого большого изменяется на значение элемента .
• « return » завершает алгоритм и выводит следующее значение.

Затем снова вставляем единицы

Algorithm ReinsertUnits
  Input: A proof $\psi _{f}$ (with a single root) and a queue $q$ of root nodes 
  Output: A proof $\psi ^{\prime }$

$\psi ^{\prime }$ ← $\psi _{f}$; 
while $q\neq \emptyset$ do
    $\eta$ ← first element of $q$;
    $q$ ← tail of $q$;
    if $\eta$ is resolvable with root of $\psi ^{\prime }$ then
        $\psi ^{\prime }$ ← resolvent of $\eta$ with the root of $\psi ^{\prime }$; 
    end 
end
return $\psi ^{\prime }$;

• « ←» означает присвоение . Например, « самый большой ← элемент » означает, что значение самого большого изменяется на значение элемента .
• « return » завершает алгоритм и выводит следующее значение.