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.
ailog: ask grandfather(G,C).
Answer: grandfather(randy,mary).
[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.
Answer: grandfather(randy,mary).
[ok,more,how,help]: more.
Answer: grandfather(randy,sue).
[ok,more,how,help]: ok.
ailog:


