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 // when KB is false, always return true
else do
P ← FIRST(symbols)
rest ← REST(symbols)
return(TT-CHECK-ALL(KB, α, rest, model ∪ { P = true })
and
TT-CHECK-ALL(KB, α, rest, model ∪ { P = false }))
Figure ?? A truth-table enumeration algorithm for deciding propositional entailment. (TT stands for truth table.) PL-TRUE? returns true if a sentence holds within a model. The variable model represents a partial model - an assignment to some of the symbols. The keyword "and" is used here as a logical operation on its two arguments, returning true or false.