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 the 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

The particularly 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 huge conjunction for all the possible assignments for the symbols occurring in the knowledge base and the query (the 'models'). About the symbols. Those are the atomic propositional representations in the vocabulary.

If you wish to know about Artificial Intelligence then visit this Artificial Intelligence Course.