我无法理解以下来自《人工智能现代方法》一书中关于命题逻辑和蕴含的算法。

用于决定命题蕴含的真值表枚举算法。TT代表真值表。PL-TRUE? 如果句子在模型中成立则返回true。变量model代表一个部分模型——仅对部分变量进行赋值。函数调用EXTEND(P, true, model)返回一个新的部分模型，其中P的值为true。

function  TT-ENTAILS? (KB,α) returns  true  or  false  inputs: KB, 知识库，一个命题逻辑中的句子           α, 查询，一个命题逻辑中的句子symbols <--- KB和α中命题符号的列表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)

回答：

当然，TT-ENTAILS所做的唯一事情就是用适当的参数调用TT-CHECK-ALL，所以这里没有太多可说的。有趣的部分从TT-CHECK-ALL的else部分开始，它递归地构造了一个针对知识库和查询中出现的符号的所有可能赋值（即‘模型’）的巨大合取式。

例如，TT-CHECK-ALL(KB, a, [P, Q], [])将被评估为

(   TT-CHECK-ALL(KB, a, [], [P=true, Q=true])    and    TT-CHECK-ALL(KB, a, [], [P=true, Q=false])) and (    TT-CHECK-ALL(KB, a, [], [P=false, Q=true])     and     TT-CHECK-ALL(KB, a, [], [P=false, Q=false]))

TT-CHECK-ALL的第一部分，当所有符号在模型中都被赋值时执行，检查给定的模型，例如[P=true, Q=false]，是否与知识库一致（PL-TRUE?(KB, model)）。这些模型对应于真值表中知识库列为true的行。对于这些模型，算法随后检查查询是否评估为true（PL-TRUE?(query, model)）。所有其他与KB不一致的模型，在一开始就被忽略，通过返回true，这是合取的中性元素。

换句话说，这与PL-TRUE?(KB, model) -> PL-TRUE?(query, model)是相同的。

简而言之，TT-CHECK-ALL检查对于与KB一致的每个模型（每个符号的‘true’或‘false’的可能赋值），查询是否评估为true：

foreach model: PL-TRUE?(KB, model) -> PL-TRUE?(query, model)

这在逻辑上等同于

not exist model: PL-TRUE?(KB, model) and not PL-TRUE?(query, model)

也就是说，不存在这样的模型，使得KB和查询的否定都可以为真，即KB和查询的否定在逻辑上是不一致的。

而这正是KB entails query的定义。

编辑：关于symbols。这些是词汇表中的原子命题符号。在书中的例子中，这些将是各种P_i,j和B_i,j，表示房间(i,j)是否有坑和/或微风。请注意，R1到R5不属于symbols的一部分，因为这些只是为了方便使用的简写，代表更复杂的术语。因此，当将KB传递给算法时，我们不会传递R1 and R2 and ... R5，而是传递(not P_1,1) and (B_1,1 <=> (P_1,2 or P_2,1)) and ... and (B_2,1)。