人工智能原理

　　7．～White(A)

Κ_B(White(B)), (4和6的进行假言推理)
　　8．～Κ_B(White(B))

White(A)，（7的逆否等价形式）
　　9． Κ_A[～Κ_B(White(B))

White(A)]，（1－5，8和规则公式7）
　　因为1－5是已知的条件。而8是1－5通过公理得到的推论，因此利用全知规则公式7：from φ├ψ and fromΚa(φ) inferΚa(ψ)，得到：Κ_A[～Κ_B(White(B))

White(A)]，这里ψ为：
　　～Κ_B(White(B))

White(A)，而φ为条件1－5。
　　10． Κ_A(～Κ_B(White(B)))

Κ_A(White(A))，（9和公理2）
　　　条件：Κ_A[～Κ_B(White(B))

White(A)]
　　　公理2：Κa(φ

ψ)

[Κa(φ)

Κa(φ

ψ)]，
　　　这里φ为～Κ_B(White(B)，ψ为White(A)
　　11． Κ_A(White(A))，（3和10的假言推理）
　　　条件：Κ_A(～Κ_B(White(B)))
　　　和Κ_A(～Κ_B(White(B)))

Κ_A(White(A))
　　　使用假言推理结论为：Κ_A(White(A))
　　为导出上述证明中的第9行，我们利用规则公式7证明，当A相信前提（1和2）时，它也相信来自前提（4，5）的一个证明结果（8）。
　　在3个聪明人问题的不同版本中，还有另外一级的嵌套推理，但是基本的策略是一样的。实际上，对于任意的k，如果假定前（k-1）人中的每个人都宣称他不知道他是否有白点，那么我们就可以对k个聪明人的问题进行求解。
　　把从公理公式（2）到公理公式（5）、普通的命题逻辑公理、普通的推理规则和规则公式（6）组合起来可以构成所谓的知识模式逻辑（modal logic of knowledge）。逻辑学家为不同的模式逻辑系统（每一个都有一个不同的公理模式）起了不同了名字。对于特定的智能体A，公理公式（2）到公理公式（5）构成的公理系统称为S5。如果去掉公理公式（5），是系统S4。如果去掉公理公式（4）和公理公式（5），是系统T。如果去掉公理公式（3），公理公式（4），公理公式（5），是系统Κ。