Proof compression

In propositional logic a resolution proof of a clause ${\displaystyle \kappa }$ 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 ${\displaystyle \kappa }$.^[1]

The DAG contains an edge from a node ${\displaystyle \eta _{1}}$ to a node ${\displaystyle \eta _{2}}$ if and only if a premise of ${\displaystyle \eta _{1}}$ is the conclusion of ${\displaystyle \eta _{2}}$. In this case, ${\displaystyle \eta _{1}}$ is a child of ${\displaystyle \eta _{2}}$, and ${\displaystyle \eta _{2}}$ is a parent of ${\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 }$.

Let's take a resolution proof for the clause ${\displaystyle \left\{a,b,c\right\}}$ from the set of clauses

${\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:

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

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

• ${\displaystyle \eta _{1}}$ and ${\displaystyle \eta _{2}}$ are parents of ${\displaystyle \eta _{3}}$
• ${\displaystyle \eta _{3}}$ is a child of ${\displaystyle \eta _{1}}$ and ${\displaystyle \eta _{2}}$
• ${\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. The resolvent of ${\displaystyle \kappa _{1}}$ and ${\displaystyle \kappa _{2}}$ with pivot ${\displaystyle p}$ can be denoted as ${\displaystyle \kappa _{1}\odot _{p}\kappa _{2}}$. When the pivot is uniquely defined or irrelevant, we omit it and write simply ${\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 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 ${\displaystyle \left\{a,b,p\right\}\odot _{p}\left\{c,\neg p\right\}}$ or simply ${\displaystyle \left\{a,b,p\right\}\odot \left\{c,\neg p\right\}.}$

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

Algorithms for compression of sequent calculus proofs include cut introduction and cut elimination.

Algorithms for compression of propositional resolution proofs include RecycleUnits,^[2] RecyclePivots,^[2] RecyclePivotsWithIntersection,^[1] LowerUnits,^[1] LowerUnivalents,^[3] Split,^[4] Reduce&Reconstruct,^[5] and Subsumption.