# Induction.

• Nov 10th 2010, 04:28 PM
tt11
Induction.
Hello

wondering if anyone is familiar with ex 3 in chapter 6 of

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
• Nov 10th 2010, 04:30 PM
Drexel28
Quote:

Originally Posted by tt11
Hello

wondering if anyone is familiar with ex 3 in chapter 6 of

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

Could you possibly just write out the problem?
• Nov 10th 2010, 04:36 PM
tt11
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.
• Nov 10th 2010, 04:49 PM
Plato
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.
• Nov 10th 2010, 07:35 PM
tt11
Thank you .... I will have a look at latex codes
• Nov 11th 2010, 10:11 AM
tt11
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)
• Nov 11th 2010, 12:48 PM
emakarov
Quote:

a1, a2 --> q1
a2, not(a3) --> q2

So in the example db above, DB union (not(a3)) would make q2 derivable.
Why is that? To derive q2, you also need a2, but there is no rule with head a2.

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.
• Nov 12th 2010, 10:26 AM
tt11
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
• Nov 12th 2010, 03:26 PM
tt11
Could you explain why f(q) < 0 is impossible?
Sorry I am missing the point
• Nov 12th 2010, 04:04 PM
emakarov
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.
• Nov 13th 2010, 01:37 PM
emakarov
OK, let's assume that stratification ranks of atoms are nonnegative integers. I'll write S(k) for $S_k$. Each S(k) is the union of $\emptyset=S(0)\subseteq S(1)\subseteq\dots$. The program DB is also a union of nested sets. Let $DB(i)=\{p\gets\vec{q}\in DB\mid f(p). Then DB is the union of $\emptyset=DB(0)\subseteq DB(1)\subseteq\dots$.

We claim that $S(\cdot,r)$ 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 $DB\cup S(k)\not\models p$. What rules from $DB\cup S(k)$ 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, $DB\cup S(k)\not \models p$ iff $DB(0)\not\models p$ and whether (not p) is in S(k + 1) does not depend on k. All in all, $S(k + 1, 1)=\{\mathbf{not}\;p\mid f(p)=0\text{ and }DB(0)\not\models p\}$ 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 $DB\cup S(r)\not\models p$. Again, concerning the DB part of $DB\cup S(r)$, 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 $DB\cup S(r)$, only its subset S(r, r) is responsible for implying p. So, we have

(not p) is in S(r + 1) iff, by definition,
$DB\cup S(r)\not\models p$ iff
$DB(r+1)\cup S(r,r)\not\models p$ iff, by assumption that S(r, r) = S(r + 1, r),
$DB(r+1),S(r+1,r)\not\models p$ iff
$DB, S(r+1)\not\models p$ iff
(not p) is in S(r + 2).

The facts that S(r + 2, r + 1) = S(r + 3, r + 1) = ... are shown similarly.
• Nov 13th 2010, 04:37 PM
tt11
You help so much