# Proof compression > Mediated Wiki article. Canonical URL: https://mediated.wiki/source/Proof_compression > Markdown URL: https://mediated.wiki/source/Proof_compression.md > Source: https://en.wikipedia.org/wiki/Proof_compression > Source revision: 1206721463 > License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/) In [proof theory](/source/Proof_theory), an area of [mathematical logic](/source/Mathematical_logic), **proof compression** is the problem of [algorithmically](/source/Algorithm) compressing [formal proofs](/source/Formal_proof). The developed algorithms can be used to improve the proofs generated by [automated theorem proving](/source/Automated_theorem_proving) tools such as [SAT solvers](/source/SAT_solver), [SMT-solvers](/source/SMT_solver), [first-order theorem provers](/source/First-order_theorem_provers) and [proof assistants](/source/Proof_assistant). ## Problem Representation In [propositional logic](/source/Propositional_logic) a [resolution](/source/Resolution_(logic)) proof of a clause κ {\displaystyle \kappa } from a set of clauses *C* is a [directed acyclic graph](/source/Directed_acyclic_graph) (DAG): the input nodes are [axiom](/source/Axiom) 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 } .[1] 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 } . ### A simple example 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: - η 1 {\displaystyle \eta _{1}} and η 2 {\displaystyle \eta _{2}} are input nodes. - The node η 3 {\displaystyle \eta _{3}} has a pivot p {\displaystyle p} , - left resolved literal p {\displaystyle p} - right resolved literal ¬ p {\displaystyle \neg p} - η 3 {\displaystyle \eta _{3}} conclusion is the clause { a , b , c } {\displaystyle \left\{a,b,c\right\}} - η 3 {\displaystyle \eta _{3}} premises are the conclusion of nodes η 1 {\displaystyle \eta _{1}} and η 2 {\displaystyle \eta _{2}} (its parents) - The DAG would be - η 1 η 2 ↖↗ η 3 {\displaystyle {\begin{array}{ccc}\eta _{1}&&\eta _{2}\\&\nwarrow \nearrow \\&\eta _{3}\end{array}}} - η 1 {\displaystyle \eta _{1}} and η 2 {\displaystyle \eta _{2}} are parents of η 3 {\displaystyle \eta _{3}} - η 3 {\displaystyle \eta _{3}} is a child of η 1 {\displaystyle \eta _{1}} and η 2 {\displaystyle \eta _{2}} - η 3 {\displaystyle \eta _{3}} is a root of the proof 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 [resolution inferences](/source/Resolution_inference). 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 [term algebra](/source/Term_algebra) 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}}} . ## Compression algorithms Algorithms for compression of [sequent calculus](/source/Sequent_calculus) proofs include [cut introduction](https://en.wikipedia.org/w/index.php?title=Cut_introduction&action=edit&redlink=1) and [cut elimination](/source/Cut_elimination). Algorithms for compression of propositional [resolution](/source/Resolution_(logic)) proofs include [RecycleUnits](/source/RecycleUnits),[2] [RecyclePivots](https://en.wikipedia.org/w/index.php?title=RecyclePivots&action=edit&redlink=1),[2] [RecyclePivotsWithIntersection](https://en.wikipedia.org/w/index.php?title=RecyclePivotsWithIntersection&action=edit&redlink=1),[1] [LowerUnits](/source/LowerUnits),[1] [LowerUnivalents](/source/LowerUnivalents),[3] [Split](/source/Resolution_proof_compression_by_splitting),[4] [Reduce&Reconstruct](/source/Resolution_proof_reduction_via_local_context_rewriting),[5] and [Subsumption](https://en.wikipedia.org/w/index.php?title=Subsumption_(logic)&action=edit&redlink=1). ## Notes 1. ^ [***a***](#cite_ref-Compression_of_Propositional_Resolution_Proofs_via_Partial_Regularization_1-0) [***b***](#cite_ref-Compression_of_Propositional_Resolution_Proofs_via_Partial_Regularization_1-1) [***c***](#cite_ref-Compression_of_Propositional_Resolution_Proofs_via_Partial_Regularization_1-2) Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno. *[Compression of Propositional Resolution Proofs via Partial Regularization](https://www.researchgate.net/profile/Bruno_Woltzenlogel_Paleo/publication/220805753_Compression_of_Propositional_Resolution_Proofs_via_Partial_Regularization/links/0deec52a5d945eb089000000.pdf)*. 23rd [Conference on Automated Deduction](/source/Conference_on_Automated_Deduction), 2011. 1. ^ [***a***](#cite_ref-Linear-time_Reductions_of_Resolution_Proofs_2-0) [***b***](#cite_ref-Linear-time_Reductions_of_Resolution_Proofs_2-1) Bar-Ilan, O.; Fuhrmann, O.; Hoory, S.; Shacham, O.; Strichman, O. *[Linear-time Reductions of Resolution Proofs](http://www.haifa.il.ibm.com/conferences/hvc2008/present/BarilanFuhrmannHooryShachamStrichman_39.pdf)*. Hardware and Software: Verification and Testing, p. 114–128, Springer, 2011. 1. **[^](#cite_ref-3)** ["Skeptik/Doc/Papers/LUniv at develop · Paradoxika/Skeptik · GitHub"](https://github.com/Paradoxika/Skeptik/tree/develop/doc/papers/LUniv). *[GitHub](/source/GitHub)*.{{[cite web](https://en.wikipedia.org/wiki/Template:Cite_web)}}: CS1 maint: deprecated archival service ([link](https://en.wikipedia.org/wiki/Category:CS1_maint:_deprecated_archival_service)) 1. **[^](#cite_ref-4)** Cotton, Scott. "[Two Techniques for Minimizing Resolution Proofs](https://link.springer.com/chapter/10.1007/978-3-642-14186-7_26)". 13th International Conference on Theory and Applications of Satisfiability Testing, 2010. 1. **[^](#cite_ref-5)** Simone, S.F.; Brutomesso, R.; Sharygina, N. "[An Efficient and Flexible Approach to Resolution Proof Reduction](https://research.ibm.com/haifa/conferences/hvc2010/present/RolliniHVCslides.pdf)". 6th Haifa Verification Conference, 2010. --- Adapted from the Wikipedia article [Proof compression](https://en.wikipedia.org/wiki/Proof_compression) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/Proof_compression?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.