## The Characteristic Clause Set

The *characteristic clause set* encodes the structure of a proof and the
essence of the cut formulas used in the proof. Its construction is based on an
analysis, which inferences go into a cut and which are propagated to the
end-sequent.
The characteristic clause set
of a skolemized
**LKDe**-proof is defined inductively.
For every node of we define:

- If is an occurrence of an axiom and is the subsequent of containing only ancestors of cut formulas then .
- Let be the predecessors of in a binary inference then
we distinguish:
- The auxiliary formulas of are ancestors of cut formulas then .
- Otherwise
, where
and is the merge of the clauses and , i.e.

- Let be the predecessor of in a unary inference then .

**Example 3**We define the

**LK**-proof (for free variables, a constant symbol):

Note that also contains non-tautological axioms.

Let be the set of the two occurrences of the cut formula
in . The ancestors of are marked by . We
compute the characteristic clause set
:

From the -marks in we first get the clause sets
corresponding to the initial sequents:

The leftmost-uppermost inference in is unary and thus the clause set corresponding to this position does not change. The first binary inference in (it is ) takes place on non-ancestors of -- the auxiliary formulas of the inference are not marked by . Consequently we obtain the set

The following inferences in are all unary and so we obtain

for being the position of the end-sequent of in .

Again the uppermost-leftmost inference in is unary and
thus does not change. The first binary inference in
takes place on ancestors of (the auxiliary
formulas are -ed) and we have to apply union to .
So we get

All following inferences in are unary leaving the clause set unchanged. Let be the occurrence of the end-sequent of in . Then the corresponding clause set is

The last inference (cut) in takes place on ancestors of and we have to apply union again. This eventually yields the characteristic clause set

It is easily verified that is unsatisfiable. This is not only a coincidence, but a general principle:

**Theorem 1**Let be a skolemized proof. Then is unsatisfiable.

In case of equational clause sets the concept of unsatisfiability has to be replaced by -unsatisfiability. For details see [6].