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)