HLK ProofTool
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 ${\rm CL}(\varphi)$ of a skolemized LKDe-proof $\varphi$ is defined inductively. For every node $\nu$ of $\varphi$ we define:

The characteristic clause set ${\rm CL}(\varphi)$ is defined as ${\mathcal C}_{\nu}$ where $\nu$ is the root node of $\varphi$. Note that for a cut-free proof $\varphi$ we have ${\rm CL}(\varphi) =
\{ \vdash \}$ (which is the set consisting just of falsum).

Example 3   We define the LK-proof $\varphi$ (for $\alpha ,\beta $ free variables, $a$ a constant symbol):

$\varphi :=$

\begin{displaymath}\infer[cut]
{(\forall x) ( \lnot P( x ) \lor Q( x ) ) \vdash (\exists y) Q( y )}
{\varphi_1 & \varphi_2 }
\end{displaymath}

$\varphi_1 :=$

\begin{displaymath}\infer[\forall:r]
{(\forall x) ( \lnot P( x ) \lor Q( x ) ) \...
...pha )^\star}
{Q( \alpha ) \vdash Q( \alpha )^\star}
}
}
}
}
}
\end{displaymath}

$\varphi_2 :=$

\begin{displaymath}\infer[\forall:l]
{(\forall x) (\exists y) ( \lnot P( x ) \lo...
...sh P( a )^\star}
& Q( \beta )^\star \vdash Q( \beta )}
}
}
}
\end{displaymath}

Note that $\varphi _2$ also contains non-tautological axioms.

Let $\Omega$ be the set of the two occurrences of the cut formula in $\varphi$. The ancestors of $\Omega$ are marked by $\star$. We compute the characteristic clause set ${\rm CL}(\varphi)$:

From the $\star$-marks in $\varphi$ we first get the clause sets corresponding to the initial sequents:

\begin{displaymath}X_1 = \{P(u) \vdash \},\ X_2 = \{ \vdash Q(u)\},\
X_3 = \{\vdash P(a)\},\ X_4 = \{Q(v) \vdash \}.\end{displaymath}

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

\begin{displaymath}Y_1 = \{P(u) \vdash \} \times \{ \vdash Q(u)\} = \{P(u) \vdash Q(u)\}.\end{displaymath}

The following inferences in $\varphi _1$ are all unary and so we obtain

\begin{displaymath}{\mathcal C}_{\nu_1} = Y_1\end{displaymath}

for $\nu_1$ being the position of the end-sequent of $\varphi _1$ in $\varphi$.

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

\begin{displaymath}Y_2 = \{\vdash P(a);\ Q(v)\vdash \}.\end{displaymath}

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

\begin{displaymath}{\mathcal C}_{\nu_2} = Y_2.\end{displaymath}

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

\begin{displaymath}{\rm CL}(\varphi ) = \{P(u) \vdash Q(u);\ \
\vdash P(a);\ \ Q(v) \vdash \}.\end{displaymath}

It is easily verified that ${\rm CL}(\varphi)$ is unsatisfiable. This is not only a coincidence, but a general principle:

Theorem 1   Let $\varphi$ be a skolemized proof. Then ${\rm CL}(\varphi)$ is unsatisfiable.

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