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.