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

## Projection and Refutation

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 [5] and [7].

The construction of is illustrated below.

Example 4   Let be the proof of the sequent

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 weakening and

For 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 .

Example 5   Let be the proof 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

Let

Moreover let us write for and for .

Then 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 .

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