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

Эта статья в значительной степени или полностью основана на одном источнике . Соответствующее обсуждение можно найти на странице обсуждения . Пожалуйста, помогите улучшить эту статью, добавив ссылки на дополнительные источники . Найти источники:  "LowerUnits" – новости  · газеты  · книги  · ученый  · JSTOR ( апрель 2014 г. )

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

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

Теорема: Пусть будет потенциально избыточным доказательством , а будет избыточным доказательством | избыточным узлом. Если предложение является единичным предложением ,${\displaystyle \varphi}$${\displaystyle \эта}$${\displaystyle \эта}$тогда это излишне.${\displaystyle \varphi}$

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

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

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

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

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

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

Алгоритм Нижние Единицы Вход: доказательство Выход: доказательство без глобальной избыточности с единичным избыточным узлом${\displaystyle \пси}$${\displaystyle \psi ^{\prime }}$

 (unitsQueue, ) ← collectUnits( ); ← исправить( );${\displaystyle \psi _{b}}$${\displaystyle \пси}$${\displaystyle \psi _{f}}$${\displaystyle \psi _{b}}$ fixedUnitsQueue ← исправить(unitsQueue); ${\displaystyle \psi ^{\prime }}$← reinsertUnits( , fixedUnitsQueue); возврат ;${\displaystyle \psi _{f}}$ ${\displaystyle \psi ^{\prime }}$

Мы собираем положения об единице следующим образом:

Алгоритм CollectUnits Вход: доказательство. Выход: пара, содержащая очередь всех узлов-единиц (unitsQueue), которые используются более одного раза , и неработающее доказательство.${\displaystyle \пси}$${\displaystyle \пси}$${\displaystyle \psi _{b}}$

${\displaystyle \psi _{b}}$← ;${\displaystyle \пси}$проход снизу вверх и foreach узел в do если это unit и имеет более одного дочернего элемента , то добавить в unitsQueue;${\displaystyle \psi _{b}}$${\displaystyle \эта}$${\displaystyle \psi _{b}}$   ${\displaystyle \эта}$${\displaystyle \эта}$${\displaystyle \эта}$ удалить из ; конец конец возврат (unitsQueue, ); ${\displaystyle \эта}$${\displaystyle \psi _{b}}$${\displaystyle \psi _{b}}$

Затем мы снова вставляем блоки.

Алгоритм ReinsertUnits Вход: Доказательство (с одним корнем) и очередь корневых узлов.${\displaystyle \psi _{f}}$${\displaystyle д}$ Вывод: Доказательство${\displaystyle \psi ^{\prime }}$

${\displaystyle \psi ^{\prime }}$← ; while do ← первый элемент ; ← хвост ; если разрешим с корнем then ← резольвента с корнем ; конец конец return ;${\displaystyle \psi _{f}}$ ${\displaystyle q\neq \emptyset }$  ${\displaystyle \эта}$${\displaystyle д}$${\displaystyle д}$${\displaystyle д}$ ${\displaystyle \эта}$${\displaystyle \psi ^{\prime }}$  ${\displaystyle \psi ^{\prime }}$${\displaystyle \эта}$${\displaystyle \psi ^{\prime }}$  ${\displaystyle \psi ^{\prime }}$