プルーフ圧縮では、LowerUnits（LU）は、命題論理分解プルーフを圧縮するために使用されるアルゴリズムです。 LowerUnitsの主なアイデアは、以下の事実を利用することです：
 定理：${\displaystyle \varphi }$は潜在的に冗長な証明とし、${\displaystyle \eta }$冗長ノード。 ${\displaystyle \eta }$の句がユニット句である場合、${\displaystyle \varphi }$は冗長です。
このアルゴリズムは、unit句を使用した複数の解像度から生じるグローバル冗長性のクラスを正確に対象としています。アルゴリズムは、この書き換えが行われ、結果の証明がDAG（有向非循環グラフ）として表示されるとき、ユニットノード${\displaystyle \eta }$が以前よりも低い（すなわち根に近い）ように見えるという事実から、元の証拠に現れます。
定理を利用した素朴な実装では、各単位ノードを下げた後に、証明を横断して修正する必要があります。ただし、最初にすべてのユニットノードを1つのトラバーサルで収集して削除し、その後、プルーフ全体を1秒間のトラバーサルで固定することで、よりうまくいく可能性があります。最後に、収集され固定されたユニットノードは、証明の底に再挿入されなければならない。
ユニットノード${\displaystyle \eta ^{\prime }}$が、別のユニットノード${\displaystyle \eta }$を派生させるサブプルーフ内で上に発生する場合には注意が必要です。このような場合、${\displaystyle \eta }$は${\displaystyle \eta ^{\prime }}$に依存する。 ${\displaystyle \ell }$を${\displaystyle \eta ^{\prime }}$の単位節の単一のリテラルとする。すると、${\displaystyle \eta }$のサブプルーフにおける${\displaystyle {\overline {\ell }}}$の出現は、${\displaystyle \eta ^{\prime }}$との解決の推論によってそれ以上取り消されない。したがって、${\displaystyle {\overline {\ell }}}$は、証明が固定されて${\displaystyle \eta }$の節に現れたときに下方に伝播する。ユニットノード${\displaystyle \eta }$を再挿入した後（すなわち、再挿入後${\displaystyle \eta ^{\prime }}$が${\displaystyle \eta }$の下に現れなければならない）、余分なリテラル${\displaystyle {\overline {\ell }}}$を取り消した後、上位ユニットノード${\displaystyle \eta ^{\prime }}$を再挿入すると、 ${\displaystyle \eta }$の節）。これは、プルーフのボトムアップ・トラバース中にキュー内の単位ノードを収集し、それらがキューに入れられた順序でそれらを再挿入することによって保証され得る。
多くのルートを含む証明を固定するためのアルゴリズムは、証明のトップダウントラバースを行い、解決法を再計算し、壊れたノード（例えば、deletedNodeMarkerをその親の1つとして持つノード）を、それらの残存する親（例えば、親はdeletedNodeMarkerでした）。
ユニットノードが節${\displaystyle \kappa }$の証明から摘出され、証明が固定されている場合、新しい証明のルートノードの節${\displaystyle \kappa ^{\prime }}$はもはや${\displaystyle \kappa }$と等しくはなく、証明から除外された単位節のリテラルの二重項。証明の根底にある単位ノードの再挿入は${\displaystyle \kappa }$の証明を再び得るために、収集された単位ノードの節（いくつかの）と${\displaystyle \kappa ^{\prime }}$を解決する。