Confusion in propositional logic algorithm

Question

I'm not able to understand the following algorithm concerning propositional logic and entailment, taken from the book Artificial Intelligence A modern approach.

A truth-table enumeration algorithm for deciding propositional entailment. TT stands for truth table. PL-TRUE? returns true if a sentence holds within a model. The variable model represents a partial model- assignment to only some of the variables. The function call EXTEND(P, true, model) returns a new partial model in which P has the value true.

function  TT-ENTAILS? (KB,α) returns  true  or  false
  inputs: KB, the knowledge base, a sentence in propositional logic
           α, the query, a sentence in propositional logic

symbols <--- a list of the propositional symbols in KB and α
return TT-CHECK-ALL(KB,α,symbols,[])

---

function TT-CHECK-ALL(KB,α,symbols,model ) returns true or false
   if EMPTY?(symbols) then
       if PL-TRUE?(KB, model) then return PL-TRUE?(α,model)
       else return true

   else do
       P <---FIRST(symbols); rest <--- REST(symbols)
       return TT-CHECK-ALL(KB,α,rest,EXTEND(P,true,model) and
              TT-CHECK-ALL(KB, α, rest, EXTEND(P,false,model)

Answer 1

Of course, the only thing TT-ENTAILS does is to call TT-CHECK-ALL with the proper parameters, so there is not much to tell here. The interesting bits start in the else part ofTT-CHECK-ALL which recursively constructs a huge conjunction for all the possible assignments for the symbols occurring in the knowledge base and the query (the 'models').

For example, TT-CHECK-ALL(KB, a, [P, Q], []) will evaluate to

(
   TT-CHECK-ALL(KB, a, [], [P=true, Q=true]) 
   and 
   TT-CHECK-ALL(KB, a, [], [P=true, Q=false])
) 
and 
(
    TT-CHECK-ALL(KB, a, [], [P=false, Q=true]) 
    and 
    TT-CHECK-ALL(KB, a, [], [P=false, Q=false])
)

The first part of TT-CHECK-ALL, which is executed when all the symbols have been given a value in the model, checks whether the given model, e.g. [P=true, Q=false], is consistent with the knowledge base (PL-TRUE?(KB, model)). These models correspond to the lines in the truth table, which have a true in the KB column. For those, the algorithm then checks whether the query evaluates to true (PL-TRUE?(query, model)). All other models, that are inconsistent with the KB in the first place, are not considered, by returning true, which is the neutral element of conjugation.

In other words, this is the same as PL-TRUE?(KB, model) -> PL-TRUE?(query, model).

So in short, TT-CHECK-ALL checks that for each model (each possible assignment of 'true' or 'false' to the different symbols) that is consistent with the KB, the query evaluates to true:

foreach model: PL-TRUE?(KB, model) -> PL-TRUE?(query, model)

Which is logically equivalent to

not exist model: PL-TRUE?(KB, model) and not PL-TRUE?(query, model)

That is, there is no model, such that KB and the negation of the query can both be true, i.e. the KB and the negation of the query are logically inconsistent.

And this is exactly the definition of KB entails query.

Edit: About the symbols. Those are the atomic propositional symbols in the vocabulary. In the example in the book those would be the various P_i,j and B_i,j, denoting whether room (i,j) has a pit and/or a breeze. Note that R1 through R5 are not part of symbols, as those are just shorthands for convenience, representing more complex terms. Consequently, when passing the KB into the algorithm we would not pass R1 and R2 and ... R5, but (not P_1,1) and (B_1,1 <=> (P_1,2 or P_2,1)) and ... and (B_2,1).