Logic for Computer Scientists/Predicate Logic/Semantic Trees

From Wikibooks, open books for an open world
< Logic for Computer Scientists‎ | Predicate Logic
Jump to: navigation, search

Semantic Trees[edit]

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[edit]

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[edit]

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[edit]

  • 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)[edit]

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)[edit]

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

Problems[edit]

Problem 10 (Predicate)[edit]

Assume the following set of clauses:

 M_0 = \{ \{p(x)\}, \{q(x,f(x)),\lnot p(x)\},\{\lnot q(g(y),z)\} \}


  1. Indicate (a) the Herbrand-universe and (b) the Herbrand-basis for M_0!
  2. Give a closed semantic tree for M_0!


\Box

Problem 11 (Predicate)[edit]

The following formulae F and G are given.


F  =  \forall y  p(y) \land \exists z  \lnot p(z)



G  =  r(a) \land \forall x (r(x) \to r(f(x)))

Give for F and G (a) a finate and (b) an infinite Herbrand model, or argument if this is not possible.
\Box

Problem 12 (Predicate)[edit]

The following sets of clauses are given:

  1. M_1 = \big\{ \{ p(a,x) \}, \{ \lnot p(y,b), q(y) \} \big\}
  2. M_2 = \big\{ \{ r(x), r(f(x)) \} \big\}

Give for each of them (a) a Herbrand universe, (b) Herbrand model and (c) a non-Herbrand model.
\Box