计算机科学家逻辑/模态逻辑/多模态逻辑 - 一个例子
如果要使用模态逻辑来表达不同代理的知识，则需要参数化的操作符：我们引入方框操作符 ，它们由任意项 参数化；对于 ，参数化的菱形操作符也是如此。
![{\displaystyle [a]}](https://wikimedia.org/api/rest_v1/media/math/render/svg/ea82bc70a8e322f13a3c4e5b9d5d69e8ef097ad8)
一位国王想要知道他的三个顾问中谁最聪明，就在他们每个人的额头上涂了一个白点，告诉他们这些点是黑点或白点，并且至少有一个白点，然后要求他们说出自己额头上的点的颜色。过了一段时间，第一个智者说：“我不知道我是否有白点。” 第二个听到后，也说自己不知道。第三个（真正！）智者然后回答：“我的点一定是白色的。”
以下是使用缩写 进行的形式化，它代表任意嵌套的参数化 操作符。如果我们只有 2 个智者 和 ， 将代表 。因此，一般来说， 代表“ 是普遍已知的”。
![{\displaystyle []}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0261e8d17bc0832139076efdad67e7c0abf21cff)
![{\displaystyle [A]F\land [B]F\land [A][B]F\land [B][A]F\land [A][A]F\cdots }](https://wikimedia.org/api/rest_v1/media/math/render/svg/ba2a70a5beb897c28125913c29ce6d7bb3649543)
这三个智者是不同的
众所周知，他们中有人有白点
众所周知，如果有人没有白点，其他人就会知道
C 知道，B 知道，A 不知道自己位置的颜色。
C 知道，B 不知道自己位置的颜色。
![{\displaystyle \square (\forall x,y:x\neq y\to (\lnot w(x)\to [y]\lnot w(x)))}](https://wikimedia.org/api/rest_v1/media/math/render/svg/0940dd8e2552adae0b42a2f66ed8bfd5fd7ce42e)
![{\displaystyle [C][B]\lnot [A]w(A)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/9630849e34209aa28a1941b36a7a965cba012353)
![{\displaystyle [C]\lnot [B]w(B)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2bd6651c3a4890a2493aada50b514976e34807b0)
要证明的定理是 " 知道自己有一个白色位置"
![{\displaystyle [C]w(c)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2c2d0dc681e3f4c75c55766c4427842b3e873a0c)
如果我们有一个模态逻辑定理证明器，我们可以将其应用于上述指定的问题，以便获得证明，从而得到定理的解释。
在本节的其余部分，我们将介绍两种定义这种定理证明器的方法：直接表格演算和翻译方法到一阶经典谓词逻辑。