Propositional Logic. Algorithm for Deciding Entailment

Question

I start studying artificial intelligence and logic. There are many things I do not know.

Reading about inference I found that a Knowledge Base KB entails a sentence a if and only if a is true in every model in KB. Then I found this algorithm for deciding entailment. I would like a brief explanation on how it works, especially the recursivity part.

function TT-ENTAILS? (KB, a) returns true or false
    inputs:  KB, the knowledge base
             a, the query, a sentence
    symbols: a list of the proposition symbols in KB and a

function TT-CHECK-ALL(KB, a, symbols, model) returns true or false
    if EMPTY?(Symbols) then
        if PL-TRUE?(KB, model) then return PL-TRUE?(a, model)
        else return true
    else do
        P = FIRST(symbols); rest = REST(symbols)
        return TT-CHECK-ALL(KB, a, rest, EXTEND(P, true, model)) and
               TT-CHECK-ALL(KB, a, rest, EXTEND(P, false, model))

Cheers!

Answer 1

The algorithm just computes every line of the truth table for the formula $KB\Rightarrow a$ and checks that it comes out true everywhere. The recursion is for constructing every combination of truth values for the symbols.