Redundant proof

In mathematical logic, a redundant proof is a proof that has a subset that is a shorter proof of the same result. That is, a proof $\psi$ of $\kappa$ is considered redundant if there exists another proof $\psi^{\prime}$ of $\kappa^{\prime}$ such that $\kappa^{\prime}\subseteq\kappa$ (i.e. $\kappa^{\prime} \;\text{subsumes}\; \kappa$) and $|\psi^{\prime}|<|\psi|$ where $|\varphi|$ is the number of nodes in $\varphi$.^[1]

Local redundancy

A proof containing a subproof of the shapes (here omitted pivots indicate that the resolvents must be uniquely defined)

$(\eta\odot\eta_1) \odot (\eta\odot\eta_2)\text{ or } \eta \odot (\eta_1 \odot (\eta\odot\eta_2))$

is locally redundant.

Indeed, both of these subproofs can be equivalently replaced by the shorter subproof $\eta \odot (\eta_1 \odot \eta_2 )$. In the case of local redundancy, the pairs of redundant inferences having the same pivot occur close to each other in the proof. However, redundant inferences can also occur far apart in the proof.

The following definition generalizes local redundancy by considering inferences with the same pivot that occur within different contexts. We write $\psi\left[\eta\right]$ to denote a proof-context $\psi\left[-\right]$ with a single placeholder replaced by the subproof $\eta$.

Global redundancy

A proof

$\psi [ \psi_1 [\eta \odot_p \eta_1 ] \odot \psi_2 [\eta\odot_{p} \eta_{2}] ]\text{ or } \psi [ \psi_1 [ \eta\odot_p ( \eta_1 \odot \psi_2 [ \eta \odot_p \eta_2 ])]]$

is potentially (globally) redundant. Furthermore, it is (globally) redundant if it can be rewritten to one of the following shorter proofs:

$\psi [ \eta \odot_p ( \psi_1 [ \eta_1 ] \odot \psi_2 [ \eta_2 ] )]\text{ or } \eta \odot_p \psi [ \psi_1 [ \eta_1 ]\odot\psi_2[\eta_2]]\text { or } \psi [ \psi_1 [ \eta_1 ] \odot \psi_2 [ \eta_2 ] ].$

Example

The proof

$\cfrac{\cfrac{\cfrac{\eta:\, p,q\,\,\,\,\eta_{1}:\,\neg p,r}{q,r}p\,\,\,\,\,\,\begin{array}{c} \\\eta_{3}:\,\neg q\end{array}}{r}q\,\,\,\,\,\,\,\,\,\,\,\,\,\cfrac{\cfrac{\eta\,\,\,\,\,\,\,\,\,\,\,\,\,\eta_{2}:\,\neg p,s,\neg r}{q,s,\neg r}p\,\,\,\,\begin{array}{c} \\\eta_{3}\end{array}}{s,\neg r}q}{\psi:\, s}r$

is locally redundant as it is an instance of the first pattern in the definition $((\eta\odot_p \eta_1) \odot \eta_3) \odot ((\eta\odot_p \eta_2) \odot \eta_3).$

• The pattern is $\psi [\psi_1 [\eta \odot_p \eta_1] \odot \psi_2 [ \eta \odot_p \eta_2 ]]$

• $\psi_1 [-] = \psi_2 [-] =\_\odot\eta_3 \text{ and }\psi [-] = \_$

But it is not globally redundant because the replacement terms according to the definition contain $\psi_1 [\eta_1] \odot \psi_2 [\eta_2]$ in all the cases and $\psi_1 [\eta_1] \odot \psi_2 [\eta_2] = (\eta_1 \odot \eta_3) \odot (\eta_2 \odot \eta_3)$ does not correspond to a proof. In particular, neither $\eta_1$ nor $\eta_2$ can be resolved with $\eta_3$, as they do not contain the literal $q$.

The second pattern of potentially globally redundant proofs appearing in global redundancy definition is related to the well-known notion of regularity. [This link to "regularity" is (obviously) a link to a disambiguation page.] Informally, a proof is irregular if there is a path from a node to the root of the proof such that a literal is used more than once as a pivot in this path.

Notes

1. Fontaine, Pascal; Merz, Stephan; Woltzenlogel Paleo, Bruno. Compression of Propositional Resolution Proofs via Partial Regularization. 23rd International Conference on Automated Deduction, 2011.