自动认识逻辑
自动认识逻辑，是致力于形式化关于知识的表示和推理的形式逻辑。命题逻辑只能表达事实，而自动认识逻辑可以表达关于事实的知识和知识的缺乏。
语法
自动认识逻辑的语法通过增加指示知识的模态算子 ◻ 而扩展了命题逻辑: 如果 F 是一个公式，则 ◻ F 指示 F 是已知。作为结果，◻ ¬ F 指示 ¬ F 是已知，而 ¬ ◻ F 指示 F 是未知。
在自动认识逻辑中的公式可以用来捕获基于事实知识的推理。例如，¬ ◻ F → ¬ F 意味着如果不知道 F 是真的，则假定它为假。这是一种形式的否定为失败。
语义
自动认识逻辑的语义基于的是理论的展开(expansion)，它扮演的角色类似于命题逻辑中的模型。命题模型指定原子哪个为真哪个为假，而展开指定公式 ◻ F 哪个为真哪个为假。特别是，自动认识公式 T 的展开对在 T 中包含的所有子公式 ◻ F 都做这种区分。这种区分允许 T 被作为命题公式处理，因为包含 ◻ 的所有子公式都要么是真要么是假。特别是，使用命题演算的规则来检查 T 在这种条件下是否蕴涵 F 。为了使初始假定是一个展开，一个子公式 F 被蕴涵是必须的当且仅当 ◻ F 已经被初始假定为真。
例如，在公式 T = ◻ x → x 中，只有一个单一的“加方框的子公式” ◻ x 。所以只有两个候选的展开，分别是假定它为真或为假。对实际上的展开所做的检查如下：
- ◻ x 为假: 通过这个假定，因为 ◻ x → x 等价于 ¬ ◻ x ∨ x ，而 ¬ ◻ x 被假定为真，T 成为重言式；所以 x 没有被蕴涵。这个结果符合在 ◻ x 为假中所暗含的假定，就是说 x 当前是未知的。所以 ◻ x 为假的假定是一个展开。
- ◻ x 为真: 通过这个假定，T 蕴涵 x ；所以在 ◻ x 为真中所暗含的初始假定，就是说 x 为真是已知的，被满足了。作为结果，这是另一个展开。
因此公式 T 有两个展开，在其中一个中 x 是未知，在另一个中 x 是已知。第二个被认为是反直觉的，因为 ◻ x 为真的初始假定只说明了为什么 x 为真，符合这个假定。换句话说，这是一个自支持的假定。允许这种信仰的自支持的逻辑叫做非强根基的，区别于在其中自支持是不可能的强根基的逻辑。自动认识逻辑的强根基变体存在。
参见
→ 学科目录： 哲学（目录）
