Every clause in the characteristic clause set of a skolemized proof defines a proof projection . is defined from by omitting all inferences on ancestors of cuts, leaving the clause 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, is a cut-free proof of the end-sequent augmented by . For a formal definition of projection we refer to  and .
The construction of is illustrated below.
as defined in Example 3. We have shown that
We now define , the projection of to :
The problem can be reduced to a projection in because the last inference in is a cut and
By skipping all inferences in leading to the cut formulas we obtain the deduction
In order to obtain the end-sequent we only need an additional
we obtain the projection :
Similarly we obtain :
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 be a proof of s.t. is skolemized and let be a ground resolution refutation of the (unsatisfiable) set of clauses . Then can be transformed into a proof of with at most atomic cuts. is constructed from simply by replacing the clauses by the corresponding proof projections. The construction of 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 can be considered as the characteristic part of representing the reduction to atomic cuts. Below we give an example of a construction of .
as defined in Examples 3 and 4. Then
First we define a resolution refutation of :
and a corresponding ground refutation :
The ground substitution defining the ground projection is
Moreover let us write for and for .
is of the form
Finally we give the general definition of CERES (cut-elimination by resolution) as a whole. As an input we take skolemized proofs .
- construct ,
- construct a resolution refutation of ,
- compute the output for a ground projection of .