Logic for Computer Scientists/Predicate Logic/Semantic Trees

Semantic Trees

In this section we introduce the concept of semantic trees, which then can be used to proof completeness of resolution. For this we assume familiarity with the concepts of trees, binary trees and paths in trees.

Definition 15

A semantic tree for a set of clauses $S$ is a binary tree $T$ with root $N_{0}$ , such that the edges are label with literals, built from elements from the Herbrand basis of $S$ , such that:

If $N$ is an inner node, its two outgoing edges are label with complementary literals $A$ and $\lnot A$ .
Every path to a node $N$ in $T$ does not contain complementary literals in $I(N)$ , where $I(N)$ is the set of literals which are labels along the edges of the path.

Definition 16

A semantic tree is called complete, if every path contains every atom from the Herbrand basis either positive or negative.

Example: $S=\{p(x),q(f(x))\}$ with Herbrand basis

\{p(a),q(a),p(f(a)),q(f(a)),p(f(f(a))),\ldots \}

Note, that for a semantic tree $T$ and a node $N$ the set $I(N)$ can be seen as an assignment of truth-values to ground atoms, as it is done in an Herbrand interpretation. Hence we call $I(N)$ a partial interpretation. A complete semantic tree corresponds to an exhaustive "enumeration" of interpretations.

Definition 17

A node $N$ of a semantic tree $T$ is a failure node if $I(N)$ falsifies some ground instance of a clause in $S$ , but $I(N')$ does not falsifiy any ground instance of a clause in $S$ for every ancestor node $N'$ of $N$ .
A semantic tree $T$ is called closed if every path contains a failure node.
A node $N$ of a closed semantic tree is called an inference node, if both immediate descendant nodes are failure nodes.

Example: $S=\{p(x),\lnot p(x)\lor q(f(x)),\lnot q(f(a))\}$ with Herbrand basis

\{p(a),q(a),p(f(a)),q(f(a)),p(f(f(a))),\ldots \}

Let $T$ be a complete semantic tree, than we call $T'$ the corresponding closed tree, if it is obtainable from $T$ by cutting all branches at a failure node.

Theorem 5 (Herbrand's Theorem - Version 1)

A set $S$ of clauses is unsatisfiable, iff for every complete semantic tree for $S$ there is a corresponding finite closed semantic tree.

Proof: Assume $S$ to be unsatisfiable and $T$ a complete semantic tree for $S$ . For every path $P$ we have the set of labels $I_{B}$ , which is an interpretation, because the tree is complete. Hence, $I_{B}$ falsifies a ground instance $C'$ of a clause $C\in S$ , because $S$ is unsatisfiable. Since there are only finitely many literals in $C'$ , there must be a failure node $N_{B}$ in a finite distance from the root. Since every path has such a failure node, there is a corresponding closed semantic tree $T'$ , which is finite.

For the opposite direction, assume that for every complete semantic tree $T$ there is a finite closed corresponding tree $T'$ . Then, every path contains a failure node, and hence, every interpretation falsifies $S$ ; hence $S$ is unsatisfiable.

Theorem 6 (Herbrand's Theorem - Version 2)

A set $S$ of clauses is unsatisfiable, iff there is a finite unsatisfiable set $S'$ of ground instances of clauses in $S$ .

Proof: Assume $S$ to be unsatisfiable and $T$ a complete semantic tree for $S$ . By Herbrand's theorem, version 1, there is a finite closed semantic tree $T'$ for $S$ . Let $S'$ be the set of ground instances of clauses, which are falsified at all failure nodes of $T'$ . $S'$ is finite and is falsified by every interpretation and hence unsatisfiable. The opposite direction we show by contraposition:

Note, that this version of Herbrand's theorem can be turned directly into a proof procedure: Given a set of clauses $S$ , for which we want to proof unsatisfiability.

Generate $S_{1}',\ldots ,S_{n}',\ldots$ sets of ground instances of clauses of $S$ . Perform a propositional test for unsatisfiability on each of them.
According to Herbrand's theorem, there is a finite $S_{N}'$ which is unsatisfiable, if $S$ is unsatisfiable.