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 : the input nodes are axiom inferences 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:
A refutation of C is a resolution proof of from C. It is a common that given a node, to refer to the clause or ’s clause meaning the conclusion clause of, and proof meaning the proof having as its only root.
In some works it can be found an algebraic representation of a resolution inference. 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.