一. 报告概况
本报告主要介绍的是在多主体（本报告中仅涉及2个主体）认知系统中知识分享程度的谱系理论。报告内容基于Lomuscio的博士论文，利用模态逻辑的工具，通过对S5系统增加公理，构建了对应于不同知识共享程度的相应系统，并证明了大部分系统的完全性。
二．问答记录
Q：表示提问 A：表示回答 S：表示补充
刘壮虎Q：（Linear order in agents’ private knowledge例子中）所有主体都是用同一个程序处理数据吗？
王彦晶A：是的，在这个例子中所有主体都是用同一个程序处理数据，只是不同主体的计算能力不同，因此一个人知道的东西比他计算能力强的人一定也会知道。但这只是知识共享的一个例子，本文并不假设主体间计算能力一定有序关系，只是做一个系统化的分析。
高珂Q：直观上我们一般是先考虑完全性，再得到公理，这个研究过程感觉有点奇怪。怎么从直观上理解这些完全性的情况？
王彦晶A：对，这个是反的。
刘壮虎S：这里是以公理划分为标准，枚举所有可能情况，完全从语法的角度先来考虑。
王强Q：这篇文章写于1999年，在这之后这些理论有没有什么发展？有没有哪几个系统得到了进一步的研究或者应用呢？
程莹莹A：目前不知道有什么具体应用，理论上说在AI领域可以发挥作用。
王强Q：不同认知主体之间的计算能力怎么确定？
程莹莹A：事先给定。
周北海Q：这个报告中讲的只是2个主体的情况，有没有考虑或者研究多主体，n个主体的情况？
程莹莹A：原文中确实没有多主体的。
王彦晶S：Lomuscio最近有一个有趣的结果，证明了在协议认证时如果对2、3个人可以，就对所有人都可以。
周北海Q：这些系统都是基于S5的，其实跟日常推理不一样，因为一般人达不到这种理想状态。之所以应用少是不是也有这个方面的原因？
王彦晶A：这个目前主要用在安全协议中，确实没有日常推理的应用。
周北海Q：在日常生活中，会不会有这种情况，三个人讨论问题，你是S5，我是S4，他是KD4，这种情况下怎么考虑？
刘壮虎A：三个人应该在一个最底层的水平上。
王彦晶S：利用模态逻辑做不了人的逻辑，模态逻辑做的都是机器的逻辑。
周北海S：我认为日常推理中还是有逻辑的。
刘壮虎S：规则不一定表示为一个公理系统，有些规则不能表示为公理系统。
王彦晶S：日常推理能写出来的规则本身就很少，不一定能写出来，或者虽然能写出来，但是很混乱的。
刘壮虎S：有的规则太复杂，用它也做不了事。
刘壮虎：文章讲得很详细，但是可以多一些背景知识方面的介绍。
三．王强评论
本次报告内容主要基于Lomuscio的博士论文，他后来又单独发表了一篇会议论文，但内容都涵盖于这篇博士论文中了。作者认为他的这篇论文有三个要点：一是超立方系统，一是对多主体系统中知识结构的检查，另一个就是我们今天讲的这部分——知识共享程度的谱系。这部分内容利用模态逻辑的工具，通过对S5系统增加公理，构建了对应于不同知识共享程度的相应系统，并证明了大部分系统的完全性。程莹莹同学的报告中也非常清晰地介绍了这些系统及其完全性的证明，整体条理也很清晰。我觉得值得改进的地方有两点：一是开头介绍的部分可以更丰富一些，对于文中出现的关键词，像“MAS”，“Knowledge Sharing”之类的最好有一个详细点的介绍；二是解释每个特征公式对应的性质时可以更直观一些。
四．王彦晶老师评论
这篇文章主要关心是，我和你的知识之间有什么联系，怎么从公理上刻画这种关系。关于后续发展应用的问题，纯粹从理论上讲，没有看到有新的系统加入这里面的公理在做。因为整个知识逻辑的领域里就不是很重视这个问题，而且这种用公理刻画的方式太强了。最近有一个发展就是希望把这种交互做到局部上。现在讨论的是框架性质，全局性的，太强了，我们很多时候只需要局部性质，用二阶逻辑可以做。
从报告中我们可以看到，很多完全性定理其实是不用证的。我们知道，所有Salquist片段中的公式加入后都有典范性质，只有McKinsey formula不在片段中，需要特殊考虑。但是在S5中，有McKinsey formula 加上传递性应该是有一阶对应的。作者猜想是典范的，但是没有证明。
由此可以看到，这种系统性工作还是有意思的，如果一个个分析讨论出来，会发现很多事一样的，剩下的不多。
文章作者是在知识时态逻辑中的领军人物，他的特点是有自己的工具。他通过时态知识逻辑发展了很多可用的工具，应用于安全协议中，算是很接地气的研究。
程莹莹同学今天的报告条理清晰，结果也很清楚明白。但后面的部分对于没有模态逻辑基础的同学可能有些难，因此前面术语部分可以多讲些。此外，尽量不要翻译slides上面的话，用自己的话说出来。原文中本来有一些错误，程莹莹同学在准备报告的过程中都更正了，这点值得表扬。
a_spectrum_of_degrees_of_knowledge_sharing146172087444.pdf