HLK ProofTool
TU Vienna logic.at Theory and Logic Group (E185-2)

Projection and Refutation

Every clause $C$ in the characteristic clause set ${\rm CL}(\varphi)$ of a skolemized proof $\varphi$ defines a proof projection $\varphi [C]$. $\varphi [C]$ is defined from $\varphi$ by omitting all inferences on ancestors of cuts, leaving the clause $C$ as a ``residue'' in the end-sequent. Equality and definition rules appearing within the input proof are propagated to the projections like any other rules. In fact, $\varphi [C]$ is a cut-free proof of the end-sequent augmented by $C$. For a formal definition of projection we refer to [5] and [7].

The construction of $\varphi [C]$ is illustrated below.

Example 4   Let $\varphi$ be the proof of the sequent

\begin{displaymath}S:(\forall x)(\neg P(x) \lor Q(x)) \vdash (\exists y)Q(y)\end{displaymath}

as defined in Example 3. We have shown that

\begin{displaymath}{\rm CL}(\varphi ) = \{P(u) \vdash Q(u);\ \
\vdash P(a);\ \ Q(v) \vdash \}.\end{displaymath}

We now define $\varphi [C_1]$, the projection of $\varphi$ to $C_1\colon P(u) \vdash Q(u)$:
The problem can be reduced to a projection in $\varphi _1$ because the last inference in $\varphi$ is a cut and

\begin{eqnarray*}
{\mathcal C}_{\nu_1} &=& \{P(u) \vdash Q(u)\}.
\end{eqnarray*}



By skipping all inferences in $\varphi _1$ leading to the cut formulas we obtain the deduction


\begin{displaymath}
\infer=[\forall :l]{P(\alpha), (\forall x)(\neg P(x) \vee Q(...
...(\alpha)\vdash P(\alpha)}
&
Q(\alpha) \vdash Q(\alpha)
}
}
\end{displaymath}

In order to obtain the end-sequent we only need an additional weakening and $\varphi [C_1] =$

\begin{displaymath}
\infer=[\forall :l]{P(\alpha), (\forall x)(\neg P(x) \vee Q(...
...(\alpha)\vdash P(\alpha)}
&
Q(\alpha) \vdash Q(\alpha)
}
}
\end{displaymath}

For $C_2 =\ \vdash P(a)$ we obtain the projection $\varphi [C_2]$:

\begin{displaymath}
\infer=[\exists :r]{(\forall x)(\neg P(x) \vee Q(x)) \vdash ...
...a)}
{
\infer[w:r]{\vdash P(a), Q(\beta)}{
\vdash P(a)
}
}
\end{displaymath}

Similarly we obtain $\varphi [C_3]$:

\begin{displaymath}
\infer=[\exists :r]{Q(\beta), (\forall x)(\neg P(x) \vee Q(x)) \vdash (\exists y)Q(y)}
{ Q(\beta) \vdash Q(\beta)}
\end{displaymath}

We have seen that, in the projections, only inferences on non-ancestors of cuts are performed. If the auxiliary formulas of a binary rule are ancestors of cuts we have to apply weakening in order to obtain the required formulas from the second premise.

Let $\varphi$ be a proof of $S$ s.t. $\varphi$ is skolemized and let $\gamma$ be a ground resolution refutation of the (unsatisfiable) set of clauses ${\rm CL}(\varphi)$. Then $\gamma$ can be transformed into a proof $\varphi (\gamma)$ of $S$ with at most atomic cuts. $\varphi (\gamma)$ is constructed from $\gamma$ simply by replacing the clauses by the corresponding proof projections. The construction of $\varphi (\gamma)$ is the essential part of the method CERES (the final elimination of atomic cuts -- provided it is possible at all -- is inessential). The resolution refutation $\gamma$ can be considered as the characteristic part of $\varphi (\gamma)$ representing the reduction to atomic cuts. Below we give an example of a construction of $\varphi (\gamma)$.

Example 5   Let $\varphi$ be the proof of

\begin{displaymath}S\colon (\forall x)(\neg P(x) \lor Q(x)) \vdash (\exists y)Q(y)\end{displaymath}

as defined in Examples 3 and 4. Then

\begin{displaymath}{\rm CL}(\varphi ) = \{C_1: P(u) \vdash Q(u);\ C_2:\ \vdash P(a);\
C_3: Q(v) \vdash \}.\end{displaymath}

First we define a resolution refutation $\delta$ of ${\rm CL}(\varphi)$:

\begin{displaymath}
\infer[R]{\vdash }{
\infer[R]{\vdash Q(a)}{\vdash P(a) & P(u) \vdash Q(u)}
&
Q(v) \vdash
}
\end{displaymath}

and a corresponding ground refutation $\gamma$:

\begin{displaymath}
\infer[R]{\vdash }{
\infer[R]{\vdash Q(a)}{\vdash P(a) & P(a) \vdash Q(a)}
&
Q(a) \vdash
}
\end{displaymath}

The ground substitution defining the ground projection is

\begin{displaymath}
\sigma: \{u \leftarrow a, v \leftarrow a\}.
\end{displaymath}

Let

\begin{displaymath}
\chi_1 = \varphi [C_1]\sigma,\ \chi_2 = \varphi [C_2]\sigma\
\mbox{and}\ \chi_3 = \varphi [C_3]\sigma.
\end{displaymath}

Moreover let us write $B$ for $(\forall x)(\neg P(x) \lor Q(x))$ and $C$ for $(\exists y) Q(y)$.

Then $\varphi (\gamma)$ is of the form

\begin{displaymath}
\infer=[{\it cut}]{B \vdash C}
{ \infer=[{\it cut}]{B \vdas...
...C,Q(a)}{(\chi_1)}
}
&
\deduce{Q(a),B \vdash C}{(\chi_3)}
}
\end{displaymath}

Finally we give the general definition of CERES (cut-elimination by resolution) as a whole. As an input we take skolemized proofs $\varphi$.

Theorem 2   CERES is a cut-elimination method, i.e., for every skolemized proof $\varphi$ of a sequent $S$, CERES produces a proof $\psi$ of $S$ s.t. $\psi$ contains at most atomic cuts.