Proof compression
In proof theory, an area of mathematical logic, proof compression is the problem of algorithmically compressing formal proofs. The developed algorithms can be used to improve the proofs generated by automated theorem proving tools such as SAT solvers, SMT-solvers, first-order theorem provers and proof assistants. Problem Representation. In propositional logic a resolution proof of a clause formula_1 from a set of clauses C is a directed acyclic graph (DAG): the input nodes are axiom inferences (without premises) whose conclusions are elements of C, the resolvent nodes are resolution inferences, and the proof has a node with  conclusion formula_1. The DAG contains an edge from a node formula_3 to a node formula_4 if and only if a premise of formula_3 is the conclusion of formula_4. In this case, formula_3 is a child of formula_4, and formula_4 is a parent of formula_3. 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 formula_1 or, in some cases, a valid proof of a subset of formula_1. A simple example. Let's take a resolution proof for the clause formula_13 from the  set of clauses Here we can see: A (resolution) refutation of C is a resolution proof of formula_34 from C. It is a common that given a node formula_35, to refer to the clause formula_35 or formula_35’s clause meaning the conclusion clause of formula_35, and (sub)proof formula_35 meaning the (sub)proof having formula_35 as its only root. In some works it can be found an algebraic representation of a resolution inference. The resolvent of formula_41 and formula_42 with pivot formula_18 can be denoted as formula_44. When the pivot is uniquely defined or irrelevant, we omit it and write simply formula_45 . In this way, the set of clauses can be seen as an algebra with a commutative operator; and terms in the corresponding 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 formula_46 or simply formula_47 We can identify formula_48 Compression algorithms. Algorithms for compression of sequent calculus proofs include Cut-introduction and Cut-elimination. Algorithms for compression of propositional resolution proofs include RecycleUnits, RecyclePivots, RecyclePivotsWithIntersection, LowerUnits, LowerUnivalents, Split, Reduce&Reconstruct, and Subsumption. Proof compression