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  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 .

The DAG contains an edge from a node  to a node  if and only if a premise of  is the conclusion of . In this case,  is a child of , and  is a parent of . 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  or, in some cases, a valid proof of a subset of .

A simple example
Let's take a resolution proof for the clause  from the set of clauses

Here we can see:
  and  are input nodes. 
 The node  has a pivot , 
 left resolved literal 
 right resolved literal 
  conclusion is the clause 
  premises are the conclusion of nodes  and  (its parents)
 The DAG would be

  and  are parents of 
  is a child of  and 
  is a root of the proof

A (resolution) refutation of C is a resolution proof of  from C. It is a common given a node , to refer to the clause  or ’s clause meaning the conclusion clause of , and (sub)proof  meaning the (sub)proof having  as its only root.

In some works can be found an algebraic representation of resolution inferences. The resolvent of  and  with pivot  can be denoted as . When the pivot is uniquely defined or irrelevant, we omit it and write simply . 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  or simply 

We can identify .

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.

Notes

Proof theory