直觉主义交互式证明的逻辑（完美知识传递的形式理论）
逻辑
2015-09-22 v3 密码学与安全
计算机科学中的逻辑
摘要
我们从经典单调非析取交互式证明 (LiP) 的现有经典对应物中，构建了一个可判定的超直觉主义正规模态逻辑，即内部化的直觉主义（因而也是析取和单调的）交互式证明 (LIiP)。直觉主义交互式证明在可能具有对抗性的通信介质 CM（被设想为一个独特的智能体）中产生持久的认识论影响，且仅在此介质中产生这种影响，即通过 CM 对证明的知识，永久地诱导其对证明目标的完美且因此是析取的知识：如果 CM 知道我的证明，那么 CM 将持久地且析取地知道我的证明目标为真。因此，直觉主义交互式证明通过传输特定的个体知识（可知的直觉主义证明），在多智能体分布式系统的通信介质中实现了析取命题知识（可析取知晓的事实）的持久传递。我们这种（必然的）以 CM 为中心的证明概念，也是对 KD45-信念的析取显式细化，并由此产生了对标准 S5-知识的此类细化。单调性而非公共性是 LiP、LIiP 及其内部化证明概念的共同点。作为副产品，我们提供了直觉主义逻辑析取性质（最初由 Goedel 证明）的一个简短的内部化证明。
引用
@article{arxiv.1309.1328,
title = {Logic of Intuitionistic Interactive Proofs (Formal Theory of Perfect Knowledge Transfer)},
author = {Simon Kramer},
journal= {arXiv preprint arXiv:1309.1328},
year = {2015}
}
备注
continuation of arXiv:1201.3667; extended start of Section 1 and 2.1; extended paragraph after Fact 1; dropped the N-rule as primitive and proved it derivable; other, non-intuitionistic family members: arXiv:1208.1842, arXiv:1208.5913