6.1 How? Questions

## 6.1 How? Questions

When the system has derived an answer you can ask how that answer was produced. This provides a mechanism for interactively traversing a proof tree. At each stage the system either says why the answer was produced immediately (e.g., if it was a fact or a built-in predicate -- see Section 8) or produces the instance of the top-level rule that was used to prove the goal.

When you ask how atom h was proved, it produces the instance of the rule in the knowledge base with h as the head that succeeded:

```h <-
1: a_1
2: a_2
...
k: a_k
```
which indicates that the rule h <- a1 & a2 & ...& ak was used to prove h. You can then give one of:
how i.
where i is an integer 1 <= i <= k. This means that you want to see how ai was proved.
up.
to go back to see the rule with h in the body. If h is the initial query it goes back to the answer interaction.
retry.
to ask for a different proof tree.
ok.
to exit the how traversal and go back to the answer prompt.
help.
for a list of the available commands.
If ai was not proved via a rule (for example, if it was a fact or a built-in predicate), the reason that ai was proved is printed and then the rule with ai in the body is printed again.

Example. Given the knowledge base after Example 4, you can ask how a particular instance of the query was proved, as in:

```cilog: ask grandfather(G,C).
[ok,more,how,help]: how.
grandfather(randy,mary) <-
1: father(randy,sally)
2: parent(sally,mary)
How? [number,up,retry,ok,help]: how 2.
parent(sally,mary) <-
1: mother(sally,mary)
How? [number,up,retry,ok,help]: how 1.
mother(sally,mary) is a fact
parent(sally,mary) <-
1: mother(sally,mary)
How? [number,up,retry,ok,help]: up.
grandfather(randy,mary) <-
1: father(randy,sally)
2: parent(sally,mary)
How? [number,up,retry,ok,help]: how 1.
father(randy,sally) is a fact
grandfather(randy,mary) <-
1: father(randy,sally)
2: parent(sally,mary)
How? [number,up,retry,ok,help]: up.