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

A simple example edit

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.