(28th-July-2020)
There are a number of properties that can be established for the proof procedure
• Soundness
• Every atom in C is a logical consequence of KB. That is, if KB g then KB g. To show this, assume that an atom exists in C that is not a logical consequence of KB. If such an element exists, there must be a first element added to C that is not true in every model of KB. Suppose this is h, and suppose it is not true in model I of KB; h must be the first element generated that is false in I. Because h has been generated, there must be some definite clause in KB of the form h←b1∧...∧bm such that b1...bm are all in C (which includes the case where h is an atomic clause and so m=0). The bi are generated before h and so are all true in I. This clause's head is false in I, and its body is true in I; therefore, by the definition of truth of clauses, this clause is false in I. This is a contradiction to the fact that I is a model of KB. Thus, every element of C is a logical consequence of KB.
Complexity
• The algorithm of Figure 5.3 halts, and the number of times the loop is repeated is bounded by the number of definite clauses in KB. This can be seen easily because each definite clause can only be used once. Thus, the time complexity of the preceding algorithm is linear in the size of the knowledge base if it can index the definite clauses so that the inner loop can be carried out in constant time.
Fixed Point
• The final C generated in the algorithm of Figure 5.3 is called a fixed point because any further application of the rule of derivation does not change C. C is the minimum fixed point because there is no smaller fixed point.
• Let I be the interpretation in which every atom in the minimum fixed point is true and every atom not in the minimum fixed point is false. To show that I must be a model of KB, suppose "h←b1∧...∧bm"∈KB is false in I. The only way this could occur is if b1,...,bm are in the fixed point, and h is not in the fixed point. By construction, the rule of derivation can be used to add h to the fixed point, a contradiction to it being the fixed point. Thus, there can be no definite clause in KB that is false in an interpretation defined by a fixed point. Thus, I is a model of KB.
Completeness
• Suppose KB g. Then g is true in every model of KB, so it is true in the model I defined by the minimum fixed point, and so it is in C, and so KB g.
• The model I defined above by the minimum fixed point is a minimum model in the sense that it has the fewest true propositions. Every other model must also assign the atoms in I to be true.
Comentarios