#### 5.3.3.1 How Did the System Prove a Goal?

The first explanation procedure allows the user to ask
"* how*"
a goal was derived.
If there is a proof for

*g*, either

*g*must be an atomic clause or there must be a rule

*g←a*

_{1}∧...∧a_{k}.such that a proof exists for each *a _{i}*.

If the system has derived *g*, and the user asks * how* in response, the system
can display the clause that was used to prove

*g*. If this clause was a rule, the user can then ask

**how**i.

which will give the rule that was used to prove *a _{i}*. The user can
continue using the

*command to explore how*

**how***g*was derived.

**Example 5.11:**In the axiomatization of Example 5.5, the user can ask the query

*. In response to the system proving this query, the user can ask*

**ask**lit_l2*. The system would reply:*

**how***lit_l*

_{2}←*light_l*

_{2}∧*live_l*

_{2}∧*ok_l*

_{2}.This is the top-level rule used to prove *lit_l _{2}*.
To find out how

*live_l*was proved, the user can ask

_{2}**how**2.

The system can return the rule used to prove *live_l _{2}*, namely,

*live_l*

_{2}←*live_w*

_{4}.To find how *live_w _{4}* was proved, the user can ask

**how**1.

The system presents the rule

*live_w*

_{4}←*live_w*

_{3}∧*up_s*

_{3}.To find how first atom in the body was proved, the user can ask

**how**1.

The first atom, *live_w _{3}*, was proved using the following rule:

*live_w*

_{3}←*live_w*

_{5}∧*ok_cb*

_{1}.To find how the second atom in the body was proved, the user can ask

**how**2.

The system will report that *ok_cb _{1}* is explicitly given.

Notice that the explanation here was only in terms of the knowledge level, and it only gave the relevant definite clauses it has been told. The user does not have to know anything about the proof procedure or the actual computation.