Proof compression

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