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

## 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 .
The characteristic clause set is defined as where is the root node of . Note that for a cut-free proof we have (which is the set consisting just of falsum).

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