认识论模态逻辑是模态逻辑的一个分支，它形式化了对知识和信念的推理。它通过模态算子扩展了命题逻辑，这些算子表达了单个智能体知道或相信什么，从而能够精确分析诸如“智能体A知道命题P”或“智能体B相信智能体A知道P”之类的陈述。该框架起源于哲学，但已成为计算机科学、经济学和人工智能中建模多智能体系统、分布式协议和博弈论场景的核心工具。
认识论模态逻辑的形式语言通常包括一组命题变量、布尔连接词以及每个智能体i的模态算子K_i，其中K_i φ读作“智能体i知道φ”。在多智能体系统中，人们常常为群体G添加公共知识（C_G φ）和分布式知识（D_G φ）的算子。标准语义由索尔·克里普克在20世纪50年代末引入，并由罗伯特·奥曼在1976年加以完善，它使用克里普克框架，该框架由一组可能世界和每个智能体的等价关系组成。公式K_i φ在世界w处为真，当且仅当φ在智能体i从w出发认为可能的所有世界中成立。
公理系统
最常见的认识论逻辑称为S5，其特征由以下公理和规则刻画。公理K表明，如果一个智能体知道一个蕴含式并且知道其前件，那么该智能体知道后件：K_i(φ → ψ) → (K_i φ → K_i ψ)。公理T表明知识蕴含真理：K_i φ → φ。公理4（正内省）表明，如果一个智能体知道φ，那么该智能体知道它知道φ：K_i φ → K_i K_i φ。公理5（负内省）表明，如果一个智能体不知道φ，那么该智能体知道它不知道φ：¬K_i φ → K_i ¬K_i φ。必然化规则允许从定理φ推导出K_i φ。
较弱的系统放宽了这些公理。逻辑KT（也称为T）省略了公理4和5，允许智能体缺乏内省能力。逻辑S4保留公理4但省略公理5，这通常用于信念而非知识。对于信念，公理T被公理D取代：B_i φ → ¬B_i ¬φ，该公理表明信念是一致的但不一定为真。这些区别在智能体拥有不完整或不正确信息的应用中很重要。
语义与可能世界
可能世界语义将知识解释为在所有认识论上可及的世界中为真。一个认识论模型M = (W, R_1, ..., R_n, V)由一组世界W、每个智能体的可达关系R_i以及一个为每个世界中的命题变量赋值的估值V组成。对于知识，每个R_i是一个等价关系（自反、对称、传递），反映了智能体无法区分在认识论上与其相同的世界。K_i φ在世界w处的真值条件为：对于所有满足w R_i v的v，M, v ⊨ φ。
公共知识由大卫·刘易斯在1969年和罗伯特·奥曼在1976年形式化，定义为“所有人都知道所有人都知道……”的无限合取。对于群体G，C_G φ成立当且仅当φ在通过G成员可达关系的任何有限序列可到达的所有世界中为真。这一概念对于分布式系统中的协调行动以及分析协议和约定至关重要。
在计算机科学与人工智能中的应用
认识论逻辑在20世纪80年代和90年代成为多智能体系统研究的基石。1985年，约瑟夫·哈尔彭和约拉姆·摩西发表了关于分布式系统中知识和公共知识的开创性工作，展示了认识论条件如何刻画协调问题（如协调攻击问题）的可解性。泥巴孩子谜题是一个经典例子，它展示了无知状态的公开宣告如何生成公共知识，并使得对高阶知识的推理成为可能。
在人工智能中，认识论逻辑为知识表示和推理提供了形式基础。它已被应用于建模基于知识的程序，其中智能体的行动取决于其知识状态。该框架还支撑了认识论规划，即智能体推理他人所知以实现目标。在博弈论中，奥曼1976年关于“同意分歧”的结果表明，如果智能体对彼此的后验信念具有公共知识，那么他们无法同意分歧，从而将认识论逻辑与经济推理联系起来。
动态认识论逻辑
动态认识论逻辑（DEL）由扬·普拉扎在1989年开发，后来由汉斯·范迪特马尔施、维贝·范德霍克和巴特尔德·库伊扩展，它添加了通过公开宣告或私人通信实现知识变化的算子。对φ的公开宣告通过移除所有φ为假的世界来变换模型，宣告算子[φ!]ψ表明ψ在宣告之后成立。该框架捕捉了诸如信息揭示、说谎和多智能体环境中欺骗等效应。
DEL已被应用于建模通信协议、安全协议和社会互动。例如，公开宣告的逻辑可以表达，在对φ进行真实宣告后，智能体相应地更新其知识，可能创造新的公共知识。该框架还处理更复杂的行动，如私人消息和同时宣告，使其成为分析信息流动的丰富工具。
近期发展与挑战
认识论逻辑继续发展，与博弈论、因果关系和机器学习相联系。研究者已探索了多智能体系统中公平分配、隐私和安全的认识论条件。认识论逻辑与概率的结合，如概率认识论逻辑，允许在不确定性下推理信念程度和知识。这在决策理论和建模对其环境保持概率信念的AI系统中具有应用。
一个开放的挑战是认识论逻辑中模型检验和可满足性的计算复杂性。对于多智能体的S5，可满足性是PSPACE完全的，而模型检验对于固定公式可以在多项式时间内完成。动态认识论逻辑通常具有更高的复杂性，某些变体是不可判定的。这些复杂性结果指导了实用推理工具的设计，并限制了大型多智能体系统中形式验证的可扩展性。
在现代AI的背景下，认识论逻辑为指定AI系统知道或不知道什么提供了形式语言，这与透明性和鲁棒性相关。Stanford AI Lab和BAIR (Berkeley AI Research)等机构的研究者已探索了认识论逻辑与Machine learning模型之间的联系，特别是在涉及Large language model对知识和不确定性推理的任务中。然而，这些应用仍是一个活跃的研究领域，截至2025年，将认识论逻辑直接整合到深度学习系统中仍处于萌芽阶段。