# Propositional Logic. Algorithm for Deciding Entailment [closed]

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!

-
I am not sure this is the place for "how does this algorithm works?" even if it is mathy in its nature. –  Asaf Karagila Nov 22 '11 at 16:29
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.