It only needs to ask an askable atom when there is a clause where the head has not already been proved, all of the non-askable atoms in the body have been proved, and the askable atoms in the body that have been asked have been answered by “yes”.

Here is a trace of AILog

ailog: load ’elect_bug2.ail’.
AILog theory elect_bug2.ail loaded. 

ailog: ask lit_l1.
Answer: lit_l1.
  Runtime since last report: 0.0 secs. 
    [ok,more,how,help]: how.
     lit_l1 <-
       1: light_l1 
       2: live_l1 
       3: ok_l1
     How? [Number,up,retry,ok,prompt,help]: how 2. 
     live_l1 <-
       1: live_w0 
     How? [Number,up,retry,ok,prompt,help]: how 1. 
     live_w0 <-
       1: live_w1 
       2: up_s2 
     How? [Number,up,retry,ok,prompt,help]: how 1. 
     live_w1 <-
       1: live_w3 
       2: up_s1 
     How? [Number,up,retry,ok,prompt,help]: how 2. 
up_s1 is a fact

The buggy clause is

up_s1.

(a) Give a model of the model of the knowledge base: The minimal model has { a, c, e, f, g } true and { b, d, h } false. Another model is where all atoms are true.

(b) Give an interpretation that is not a model of the knowledge base: The interpretation with a false, and all other atoms true is not a model as the first clause is false in this interpretation. The interpretation with all atoms false is not a model as the 7th clause is false in this interpretation.

(c) Give two atoms that are logical consequences of the KB: Any two of { a, c, e, f, g } .

(d) Give two atoms that are not logical consequences of the KB: Any two of { b, d, h } .