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: