# 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!

-

## closed as off topic by Asaf Karagila, Carl Mummert, Sasha, t.b., Guess who it is.Dec 5 '11 at 18:23

Questions on Mathematics Stack Exchange are expected to relate to math within the scope defined by the community. Consider editing the question or leaving comments for improvement if you believe the question can be reworded to fit within the scope. Read more about reopening questions here. If this question can be reworded to fit the rules in the help center, please edit the question.

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.