Hello
wondering if anyone is familiar with ex 3 in chapter 6 of
http://books.google.ca/books?id=OuPtLaA5QjoC&printsec=frontcover&dq=brach man+and+levesque&hl=en&ei=wzXbTKmAAsSyngeK9qkW&sa= X&oi=book_result&ct=book-thumbnail&resnum=3&ved=0CDYQ6wEwAg#v=onepage&q&f=f alse
http://www.cs.sfu.ca/CC/882/jim/ProblemSets.pdf
I appreciate any hints, as I am struggling with proving even the base case.
Thanks
Thanks for the post. The question might contain some special char, but you may refer to it in the second link (http://www.cs.sfu.ca/CC/882/jim/ProblemSets.pdf
)
The first link is for background if required.
I see that you are new to this forum, welcome.
But, if you really expect help, we must be able to read the question.
Therefore, why not learn to post in symbols? You can use LaTeX tags.
It does require some effort on your part. But the reward is worth the effort.
We have a ranked db, and it is made up of antecedents and consequents like
a1, a2 --> q1
a2, not(a3) --> q2
….
it is ranked in the sense that there is function f which assigns to atoms numbers such that for every rule, and every i (between 1 and n), f(q) > = f(ai) and f(not(ai)) = 1+f(ai); the conclusion of the rule assigned g higher than all negative atoms.
It is possible to construct a set of atoms that cannot be derived from this db through reasoning, in an iterative fashion. We can construct a set, Sk = {not(a3), not(a4), ..} if we were to add these to the
DB and perform logical reasoning, , the set of atoms we could not derive would be the ones in Sk.
starting with S0={} and then building list gradually, until Sk is equal to Sk+1 (sequence converges).
S0 = {}
Sk+1 = {not(q) |DB union Sk |/= q }
So in the example db above, DB union (not(a3)) would make q2 derivable. Now we define two natural numbers k, r. S(k, r) = {not(q) ∈ Sk | f(q) < r}. It is possible to verify that for any k, ai, where f(p)= r
DB Union Sk |= p iff DB Union S(k, r) |= p., meaning, to prove p, we only need to look at the negative atoms (not(ai)) that have lower f(ai) than p.
The question is that, for a r < k, we should show S(k+1,r) = S(k+2, r)
For base case, I assume k=1, r=0. For induction, I should show if S(k+1,r) = S(k+2, r) then S(k+2,r) = S(k+3, r). After working on this for a while, I have some ideas about the base case, although not very clear. Can someone recommend some hints or reading material on how to begin transforming induction case to goal case?
Thanks (I know it is a very long question)
Why is that? To derive q2, you also need a2, but there is no rule with head a2.a1, a2 --> q1
a2, not(a3) --> q2
…
So in the example db above, DB union (not(a3)) would make q2 derivable.
The base case is S(2, 0) = S(3, 0), and it is trivial because by the definition of S(k, r), the set S(k, 0) is empty for any k (f(q) < 0 is impossible).
I'll think more about the induction step tomorrow.
First of all thank you very much for the reply.
Yes, you are right about a2. I forgot to mention that, or other facts. (like a1, ...) . I will go through the base case explanation that you provided and looking forward to your help for the induction step.
Thanks again
I assumed that f maps atoms to natural numbers, though the definition does not say so. Since the DB is probably finite, it does not matter, but if f maps atoms to integers, I believe the induction's base case should deal with k that is the minimum value of f on any atom.
OK, let's assume that stratification ranks of atoms are nonnegative integers. I'll write S(k) for . Each S(k) is the union of . The program DB is also a union of nested sets. Let . Then DB is the union of .
We claim that stabilizes after r steps, i.e., S(r, r) = S(r + 1, r) = S(r + 2, r) = ... Why? Suppose that f(p) = 0 for some p. Then for any k >= 0, (not p) is in S(k + 1), by definition, iff . What rules from determines if p is implied? Since f(p) = 0, these rules don't have "not" in them, i.e., they are in DB(0). This also means that S(k), which consists of negative literals (i.e., negations of atoms) don't play a role in whether p is implied. Thus, iff and whether (not p) is in S(k + 1) does not depend on k. All in all, for any k >= 0, so S(1, 1) = S(2, 1) = ...
Now, suppose that r >= 1 and it has been shown that S(r, r) = S(r + 1, r) = S(r + 2, r) = ... We would like to show that S(r + 1, r + 1) = S(r + 2, r + 1) = ... Suppose that f(p) < r + 1. By definition, (not p) is in S(r + 1) iff . Again, concerning the DB part of , only its subset DB(r + 1) is responsible for implying p, and if (not q) occurs in DB(r + 1) for some q, then f(q) < r. Therefore, of the S(r) part of , only its subset S(r, r) is responsible for implying p. So, we have
(not p) is in S(r + 1) iff, by definition,
iff
iff, by assumption that S(r, r) = S(r + 1, r),
iff
iff
(not p) is in S(r + 2).
The facts that S(r + 2, r + 1) = S(r + 3, r + 1) = ... are shown similarly.