計算機科學家邏輯/模態邏輯/多模態邏輯 - 一個例子
如果要使用模態邏輯來表達不同代理的知識，則需要引數化的運算子：我們引入方框運算子 ，它們由任意項 引數化；對於 ，引數化的菱形運算子也是如此。
![{\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)
如果我們有一個模態邏輯定理證明器，我們可以將其應用於上述指定的問題，以便獲得證明，從而得到定理的解釋。
在本節的其餘部分，我們將介紹兩種定義這種定理證明器的方法：直接表格演算和翻譯方法到一階經典謂詞邏輯。