## 6.4 Why? Questions

If you find yourself at a particular subgoal, it is often useful to find out **why** that subgoal is being proved.

When you ask why an atom was being asked, AILog produces the instance of the rule in the knowledge base with the atom in the body, such that the head was trying to be proved. This is of the form:

h <- 1: a_1 2: a_2 ... ** j: a_j ... k: a_k

This means that a_{j} is the atom that is being asked, the atoms a_{1}...a_{j-1} have been proved, and a_{j+1}...a_{k} have still to be proved.
When this is presented you can ask one of:

- how i.
- where i is an integer 1 <= i < j. This means that you want to see how a
_{i}was proved. This enters the how dialog. - how j.
- This means that you want to see how AILog is trying to prove a
_{j}(the atom you have previously asked why about). This returns to the rule with a_{j}in the body. - why.
- to see the rule with h in the body.
- prompt.
- to return to the AILog prompt.
- help.
- for a list of the available commands.

Note that you can't ask **how** i for i>j as there is no
proof tree for the atoms a_{j+1}...a_{k}. Also, AILog does not
guarantee that the rule
given will have the atoms in the body in the same order as in the
knowledge base; AILog is free to change the order of atoms in a
body as long as this doesn't introduce an error.

**Example.**

*The following shows a trace of a looping program that reaches the depth bound. We first increase the depth-bound, and then explore where the depth-bound was reached.*

ailog:tell a <- b & c & d.ailog:tell b <- e.ailog:tell e.ailog:tell c <- f & d & g.ailog:tell f <- b & h.ailog:tell h.ailog:tell d <- a.ailog:ask a.Query failed due to depth-bound 30. [New-depth-bound,where,ok,help]:50.Query failed due to depth-bound 50. [New-depth-bound,where,ok,help]:where.Depth-bound reached. Current subgoal: e [fail,succeed,proceed,why,ok,help]:why.e is used in the rule b <- ** 1: e [Number,why,help,ok]:why.b is used in the rule a <- ** 1: b 2: c 3: d [Number,why,help,ok]:why.a is used in the rule d <- ** 1: a [Number,why,help,ok]:why.d is used in the rule c <- 1: f ** 2: d 3: g [Number,why,help,ok]:how 1.f <- 1: b 2: h How? [Number,up,retry,ok,help]:how 2.h is a fact f <- 1: b 2: h How? [Number,up,retry,ok,help]:up.d is used in the rule c <- 1: f ** 2: d 3: g [Number,why,help,ok]:why.c is used in the rule a <- 1: b ** 2: c 3: d [Number,why,help,ok]:ok.Depth-bound reached. Current subgoal:e [fail,succeed,proceed,why,ok,help]:fail.No more answers. ailog: