Proof compression

<h2 id="problem-representation">Problem Representation</h2>
In <a href="/facts/Propositional_logic/MNt5v31V">propositional logic</a> a <a href="/facts/Resolution_(logic)/16uDqkcD">resolution</a> proof of a clause 
 
 
 
 κ
 
 
 {\displaystyle \kappa }
 
 from a set of clauses C is a <a href="/facts/Directed_acyclic_graph/k6zq1os9">directed acyclic graph</a> (DAG): the input nodes are <a href="/facts/Axiom/mLjP14Mc">axiom</a> inferences (without premises) whose conclusions are elements of C, the resolvent nodes are resolution inferences, and the proof has a node with conclusion 
 
 
 
 κ
 
 
 {\displaystyle \kappa }
 
.<a class="footnote-ref" id="fnref:1" href="#fn:1">1</a>
The DAG contains an edge from a node 
 
 
 
 
 η
 
 1
 
 
 
 
 {\displaystyle \eta _{1}}
 
 to a node 
 
 
 
 
 η
 
 2
 
 
 
 
 {\displaystyle \eta _{2}}
 
 if and only if a premise of 
 
 
 
 
 η
 
 1
 
 
 
 
 {\displaystyle \eta _{1}}
 
 is the conclusion of 
 
 
 
 
 η
 
 2
 
 
 
 
 {\displaystyle \eta _{2}}
 
. In this case, 
 
 
 
 
 η
 
 1
 
 
 
 
 {\displaystyle \eta _{1}}
 
 is a child of 
 
 
 
 
 η
 
 2
 
 
 
 
 {\displaystyle \eta _{2}}
 
, and 
 
 
 
 
 η
 
 2
 
 
 
 
 {\displaystyle \eta _{2}}
 
 is a parent of 
 
 
 
 
 η
 
 1
 
 
 
 
 {\displaystyle \eta _{1}}
 
. A node with no children is a root.
A proof compression algorithm will try to create a new DAG with fewer nodes that represents a valid proof of 
 
 
 
 κ
 
 
 {\displaystyle \kappa }
 
 or, in some cases, a valid proof of a subset of 
 
 
 
 κ
 
 
 {\displaystyle \kappa }
 
.

<h3>A simple example</h3>
Let's take a resolution proof for the clause 
 
 
 
 
 {
 
 a
 ,
 b
 ,
 c
 
 }
 
 
 
 {\displaystyle \left\{a,b,c\right\}}
 
 from the set of clauses

{
          
            
              η
              
                1
              
            
            :
            
              {
              
                a
                ,
                b
                ,
                p
              
              }
            
            ,
            
              η
              
                2
              
            
            :
            
              {
              
                c
                ,
                ¬
                p
              
              }
            
          
          }
        
        
        
          
            
              
                η
                
                  1
                
              
              :
              a
              ,
              b
              ,
              p
              
              
              
                η
                
                  2
                
              
              :
              c
              ,
              ¬
              p
            
            
              
                η
                
                  3
                
              
              :
              a
              ,
              b
              ,
              c
            
          
        
        p
      
    
    {\displaystyle \left\{\eta _{1}:\left\{a,b,p\right\},\eta _{2}:\left\{c,\neg p\right\}\right\}\quad {\frac {\eta _{1}:a,b,p\quad \quad \eta _{2}:c,\neg p}{\eta _{3}:a,b,c}}p}

Here we can see:

<ul><li>
 
 
 
 
 η
 
 1
 
 
 
 
 {\displaystyle \eta _{1}}
 
 and 
 
 
 
 
 η
 
 2
 
 
 
 
 {\displaystyle \eta _{2}}
 
 are input nodes.</li>
<li>The node 
 
 
 
 
 η
 
 3
 
 
 
 
 {\displaystyle \eta _{3}}
 
 has a pivot 
 
 
 
 p
 
 
 {\displaystyle p}
 
,
<ul><li>left resolved literal 
 
 
 
 p
 
 
 {\displaystyle p}
 
</li>
<li>right resolved literal 
 
 
 
 ¬
 p
 
 
 {\displaystyle \neg p}
 
</li></ul></li>
<li>
 
 
 
 
 η
 
 3
 
 
 
 
 {\displaystyle \eta _{3}}
 
 conclusion is the clause 
 
 
 
 
 {
 
 a
 ,
 b
 ,
 c
 
 }
 
 
 
 {\displaystyle \left\{a,b,c\right\}}
 
</li>
<li>
 
 
 
 
 η
 
 3
 
 
 
 
 {\displaystyle \eta _{3}}
 
 premises are the conclusion of nodes 
 
 
 
 
 η
 
 1
 
 
 
 
 {\displaystyle \eta _{1}}
 
 and 
 
 
 
 
 η
 
 2
 
 
 
 
 {\displaystyle \eta _{2}}
 
 (its parents)</li>
<li>The DAG would be</li></ul>

η
                  
                    1
                  
                
              
              
              
                
                  η
                  
                    2
                  
                
              
            
            
              
              
                ↖↗
              
            
            
              
              
                
                  η
                  
                    3
                  
                
              
            
          
        
      
    
    {\displaystyle {\begin{array}{ccc}\eta _{1}&&\eta _{2}\\&\nwarrow \nearrow \\&\eta _{3}\end{array}}}

<ul><li>
 
 
 
 
 η
 
 1
 
 
 
 
 {\displaystyle \eta _{1}}
 
 and 
 
 
 
 
 η
 
 2
 
 
 
 
 {\displaystyle \eta _{2}}
 
 are parents of 
 
 
 
 
 η
 
 3
 
 
 
 
 {\displaystyle \eta _{3}}
 
</li>
<li>
 
 
 
 
 η
 
 3
 
 
 
 
 {\displaystyle \eta _{3}}
 
 is a child of 
 
 
 
 
 η
 
 1
 
 
 
 
 {\displaystyle \eta _{1}}
 
 and 
 
 
 
 
 η
 
 2
 
 
 
 
 {\displaystyle \eta _{2}}
 
</li>
<li>
 
 
 
 
 η
 
 3
 
 
 
 
 {\displaystyle \eta _{3}}
 
 is a root of the proof</li></ul>
A (resolution) refutation of C is a resolution proof of 
 
 
 
 ⊥
 
 
 {\displaystyle \bot }
 
 from C. It is a common given a node 
 
 
 
 η
 
 
 {\displaystyle \eta }
 
, to refer to the clause 
 
 
 
 η
 
 
 {\displaystyle \eta }
 
 or 
 
 
 
 η
 
 
 {\displaystyle \eta }
 
’s clause meaning the conclusion clause of 
 
 
 
 η
 
 
 {\displaystyle \eta }
 
, and (sub)proof 
 
 
 
 η
 
 
 {\displaystyle \eta }
 
 meaning the (sub)proof having 
 
 
 
 η
 
 
 {\displaystyle \eta }
 
 as its only root.
In some works can be found an algebraic representation of <a href="/facts/Resolution_inference/IcBv9atk">resolution inferences</a>. The resolvent of 
 
 
 
 
 κ
 
 1
 
 
 
 
 {\displaystyle \kappa _{1}}
 
 and 
 
 
 
 
 κ
 
 2
 
 
 
 
 {\displaystyle \kappa _{2}}
 
 with pivot 
 
 
 
 p
 
 
 {\displaystyle p}
 
 can be denoted as 
 
 
 
 
 κ
 
 1
 
 
 
 ⊙
 
 p
 
 
 
 κ
 
 2
 
 
 
 
 {\displaystyle \kappa _{1}\odot _{p}\kappa _{2}}
 
. When the pivot is uniquely defined or irrelevant, we omit it and write simply 
 
 
 
 
 κ
 
 1
 
 
 ⊙
 
 κ
 
 2
 
 
 
 
 {\displaystyle \kappa _{1}\odot \kappa _{2}}
 
. In this way, the set of clauses can be seen as an algebra with a commutative operator; and terms in the corresponding <a href="/facts/Term_algebra/kRGlTKMq">term algebra</a> denote resolution proofs in a notation style that is more compact and more convenient for describing resolution proofs than the usual graph notation.
In our last example the notation of the DAG would be 
 
 
 
 
 {
 
 a
 ,
 b
 ,
 p
 
 }
 
 
 ⊙
 
 p
 
 
 
 {
 
 c
 ,
 ¬
 p
 
 }
 
 
 
 {\displaystyle \left\{a,b,p\right\}\odot _{p}\left\{c,\neg p\right\}}
 
 or simply 
 
 
 
 
 {
 
 a
 ,
 b
 ,
 p
 
 }
 
 ⊙
 
 {
 
 c
 ,
 ¬
 p
 
 }
 
 .
 
 
 {\displaystyle \left\{a,b,p\right\}\odot \left\{c,\neg p\right\}.}

We can identify 
 
 
 
 
 
 
 
 
 
 
 
 {
 
 a
 ,
 b
 ,
 p
 
 }
 
 ⏞
 
 
 
 
 η
 
 1
 
 
 
 
 ⊙
 
 
 
 
 {
 
 c
 ,
 ¬
 p
 
 }
 
 ⏞
 
 
 
 
 η
 
 2
 
 
 
 
 
 ⏟
 
 
 
 
 η
 
 3
 
 
 
 
 
 
 {\displaystyle \underbrace {\overbrace {\left\{a,b,p\right\}} ^{\eta _{1}}\odot \overbrace {\left\{c,\neg p\right\}} ^{\eta _{2}}} _{\eta _{3}}}
 
.

<h2 id="compression-algorithms">Compression algorithms</h2>
Algorithms for compression of <a href="/facts/Sequent_calculus/62NMylhL">sequent calculus</a> proofs include cut introduction and <a href="/facts/Cut_elimination/o9nltnr0">cut elimination</a>.
Algorithms for compression of propositional <a href="/facts/Resolution_(logic)/16uDqkcD">resolution</a> proofs include 
<a href="/facts/RecycleUnits/yb3zl3XI">RecycleUnits</a>,<a class="footnote-ref" id="fnref:2" href="#fn:2">2</a>
RecyclePivots,<a class="footnote-ref" id="fnref:3" href="#fn:3">3</a>
RecyclePivotsWithIntersection,<a class="footnote-ref" id="fnref:4" href="#fn:4">4</a>
<a href="/facts/LowerUnits/T6KLLTkX">LowerUnits</a>,<a class="footnote-ref" id="fnref:5" href="#fn:5">5</a>
<a href="/facts/LowerUnivalents/uS0CzUv6">LowerUnivalents</a>,<a class="footnote-ref" id="fnref:6" href="#fn:6">6</a>
<a href="/facts/Resolution_proof_compression_by_splitting/Xe1thvmF">Split</a>,<a class="footnote-ref" id="fnref:7" href="#fn:7">7</a>
<a href="/facts/Resolution_proof_reduction_via_local_context_rewriting/SNCf7JxX">Reduce&Reconstruct</a>,<a class="footnote-ref" id="fnref:8" href="#fn:8">8</a> and Subsumption.

<h2 id="notes">Notes</h2>

<h2 id="references">References</h2>

<ol>
<li id="fn:1">Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno. Compression of Propositional Resolution Proofs via Partial Regularization. 23rd Conference on Automated Deduction, 2011. <a href="https://www.researchgate.net/profile/Bruno_Woltzenlogel_Paleo/publication/220805753_Compression_of_Propositional_Resolution_Proofs_via_Partial_Regularization/links/0deec52a5d945eb089000000.pdf" target="_blank">https://www.researchgate.net/profile/Bruno_Woltzenlogel_Paleo/publication/220805753_Compression_of_Propositional_Resolution_Proofs_via_Partial_Regularization/links/0deec52a5d945eb089000000.pdf</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></li>
<li id="fn:2">Bar-Ilan, O.; Fuhrmann, O.; Hoory, S.; Shacham, O.; Strichman, O. Linear-time Reductions of Resolution Proofs. Hardware and Software: Verification and Testing, p. 114–128, Springer, 2011. <a href="http://www.haifa.il.ibm.com/conferences/hvc2008/present/BarilanFuhrmannHooryShachamStrichman_39.pdf" target="_blank">http://www.haifa.il.ibm.com/conferences/hvc2008/present/BarilanFuhrmannHooryShachamStrichman_39.pdf</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></li>
<li id="fn:3">Bar-Ilan, O.; Fuhrmann, O.; Hoory, S.; Shacham, O.; Strichman, O. Linear-time Reductions of Resolution Proofs. Hardware and Software: Verification and Testing, p. 114–128, Springer, 2011. <a href="http://www.haifa.il.ibm.com/conferences/hvc2008/present/BarilanFuhrmannHooryShachamStrichman_39.pdf" target="_blank">http://www.haifa.il.ibm.com/conferences/hvc2008/present/BarilanFuhrmannHooryShachamStrichman_39.pdf</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></li>
<li id="fn:4">Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno. Compression of Propositional Resolution Proofs via Partial Regularization. 23rd Conference on Automated Deduction, 2011. <a href="https://www.researchgate.net/profile/Bruno_Woltzenlogel_Paleo/publication/220805753_Compression_of_Propositional_Resolution_Proofs_via_Partial_Regularization/links/0deec52a5d945eb089000000.pdf" target="_blank">https://www.researchgate.net/profile/Bruno_Woltzenlogel_Paleo/publication/220805753_Compression_of_Propositional_Resolution_Proofs_via_Partial_Regularization/links/0deec52a5d945eb089000000.pdf</a> <a href="#fnref:4" class="footnote-back-ref">↩</a></li>
<li id="fn:5">Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno. Compression of Propositional Resolution Proofs via Partial Regularization. 23rd Conference on Automated Deduction, 2011. <a href="https://www.researchgate.net/profile/Bruno_Woltzenlogel_Paleo/publication/220805753_Compression_of_Propositional_Resolution_Proofs_via_Partial_Regularization/links/0deec52a5d945eb089000000.pdf" target="_blank">https://www.researchgate.net/profile/Bruno_Woltzenlogel_Paleo/publication/220805753_Compression_of_Propositional_Resolution_Proofs_via_Partial_Regularization/links/0deec52a5d945eb089000000.pdf</a> <a href="#fnref:5" class="footnote-back-ref">↩</a></li>
<li id="fn:6">"Skeptik/Doc/Papers/LUniv at develop · Paradoxika/Skeptik · GitHub". GitHub. Archived from the original on 11 April 2013. <a href="https://archive.today/20130411003024/https://github.com/Paradoxika/Skeptik/tree/develop/doc/papers/LUniv" target="_blank">https://archive.today/20130411003024/https://github.com/Paradoxika/Skeptik/tree/develop/doc/papers/LUniv</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></li>
<li id="fn:7">Cotton, Scott. "Two Techniques for Minimizing Resolution Proofs". 13th International Conference on Theory and Applications of Satisfiability Testing, 2010. <a href="https://link.springer.com/chapter/10.1007/978-3-642-14186-7_26" target="_blank">https://link.springer.com/chapter/10.1007/978-3-642-14186-7_26</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></li>
<li id="fn:8">Simone, S.F.; Brutomesso, R.; Sharygina, N. "An Efficient and Flexible Approach to Resolution Proof Reduction". 6th Haifa Verification Conference, 2010. <a href="https://research.ibm.com/haifa/conferences/hvc2010/present/RolliniHVCslides.pdf" target="_blank">https://research.ibm.com/haifa/conferences/hvc2010/present/RolliniHVCslides.pdf</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></li>
</ol>

Proof compression open-in-new

Proof compression