Third edition of Artificial Intelligence: foundations of computational agents, Cambridge University Press, 2023 is now available (including the full text).
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
such that a proof exists for each ai.
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
which will give the rule that was used to prove ai. The user can continue using the how command to explore how g was derived.
light_l2 ∧
live_l2 ∧
ok_l2.
This is the top-level rule used to prove lit_l2. To find out how live_l2 was proved, the user can ask
The system can return the rule used to prove live_l2, namely,
live_w4.
To find how live_w4 was proved, the user can ask
The system presents the rule
live_w3 ∧
up_s3.
To find how first atom in the body was proved, the user can ask
The first atom, live_w3, was proved using the following rule:
live_w5 ∧
ok_cb1.
To find how the second atom in the body was proved, the user can ask
The system will report that ok_cb1 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.
