交互式证明的逻辑（知识传递的形式理论）

我们提出交互式证明的逻辑，作为交互式计算的直觉主义基础框架，该基础是通过直觉主义逻辑的 Goedel-McKinsey-Tarski-Artemov 定义（嵌入经典证明模态逻辑）以及直觉主义证明与类型化程序之间的 Curry-Howard 同构的交互类比构造的。我们的交互式证明在其同行评审社区中产生持久的认识论影响，即通过解释评审者所掌握的（个体）证明知识，诱导出其证明目标（命题）知识。也就是说，交互式证明在多智能体分布式系统中通过传递特定个体知识（可知证明）来实现命题知识（可知事实）的传递。换言之，我们作为一个社区可以拥有形式化的公共知识：证明是这样一种事物，如果我们的同行成员之一知道它，就会在该成员身上诱导出其证明目标的知识。最后但同样重要的是，我们证明了在简单类型化交互组合逻辑中可定义的非平凡交互式计算，与简单类型化组合逻辑定义的非交互式计算具有同等能力。