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 is a binary tree with root , such that the edges are label with literals, built from elements from the Herbrand basis of , such that: If is an inner node, its two outgoing edges are label with complementary literals and . Every path to a node in does not contain complementary literals in , where 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: with Herbrand basis Note, that for a semantic tree and a node the set can be seen as an assignment of truth-values to ground atoms, as it is done in an Herbrand interpretation. Hence we call a partial interpretation. A complete semantic tree corresponds to an exhaustive "enumeration" of interpretations. Definition 17 A node of a semantic tree is a failure node if falsifies some ground instance of a clause in , but does not falsifiy any ground instance of a clause in for every ancestor node of . A semantic tree is called closed if every path contains a failure node. A node of a closed semantic tree is called an inference node, if both immediate descendant nodes are failure nodes. Example: with Herbrand basis Let be a complete semantic tree, than we call the corresponding closed tree, if it is obtainable from by cutting all branches at a failure node. Theorem 5 (Herbrand's Theorem - Version 1) A set of clauses is unsatisfiable, iff for every complete semantic tree for there is a corresponding finite closed semantic tree. Proof: Assume to be unsatisfiable and a complete semantic tree for . For every path we have the set of labels , which is an interpretation, because the tree is complete. Hence, falsifies a ground instance of a clause , because is unsatisfiable. Since there are only finitely many literals in , there must be a failure node in a finite distance from the root. Since every path has such a failure node, there is a corresponding closed semantic tree , which is finite. For the opposite direction, assume that for every complete semantic tree there is a finite closed corresponding tree . Then, every path contains a failure node, and hence, every interpretation falsifies ; hence is unsatisfiable. Theorem 6 (Herbrand's Theorem - Version 2) A set of clauses is unsatisfiable, iff there is a finite unsatisfiable set of ground instances of clauses in . Proof: Assume to be unsatisfiable and a complete semantic tree for . By Herbrand's theorem, version 1, there is a finite closed semantic tree for . Let be the set of ground instances of clauses, which are falsified at all failure nodes of . 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 , for which we want to proof unsatisfiability. Generate sets of ground instances of clauses of . Perform a propositional test for unsatisfiability on each of them. According to Herbrand's theorem, there is a finite which is unsatisfiable, if is unsatisfiable. Problems Problem 10 (Predicate) Assume the following set of clauses: Indicate (a) the Herbrand-universe and (b) the Herbrand-basis for ! Give a closed semantic tree for ! Problem 11 (Predicate) The following formulae and are given. Give for and (a) a finate and (b) an infinite Herbrand model, or argument if this is not possible. Problem 12 (Predicate) The following sets of clauses are given: Give for each of them (a) a Herbrand universe, (b) Herbrand model and (c) a non-Herbrand model.