本次报告主要从一个简单的例子“泥孩”出发，通过探讨其在基本知识逻辑（EL）和公开宣告逻辑（PAL）系统中的形式化证明过程，从中发现如何（利用自己的知识去）推导别人的知识，并将这一推理能力抽象成证明系统中显现表示的规则及公理：（一）如果3为有效公式，则*1……*n 3成立；（二）如果3是布尔公式，则[3]*1……*n 3成立。另外还探讨了“泥孩”例子中的背景知识不必要是common knowledge，以及语义模型与形式化场景的完全性对应证明的必要，最后一部分联系刑法中相关“明知”条款，探索其中的“明知”推导情形。
Q：表示提问 A：表示回答 S：表示补充
李大柱Q：EL中是不是可以通过CG算子推理别人的知识？
王彦晶A：当然有CG时是明显的，但是即使没有CG，在普通的EL系统中也可以做这样的推理。那么在这种没有CG情况下究竟是如何推理的，这个并不明显。
刘壮虎Q：K1为什么知道后面那些事情（K2m2→r2）？
王彦晶A: 这是我们的假设，应该把假设讲清楚。我们会用两个逻辑讨论今天的问题，两个逻辑的抽象程度是不一样的。后一种逻辑里会把一些动作以及announcement考虑到对象语言中去，更加细致；而在最基本的知识的逻辑里，没有办法直接讨论动作，所以只能假设announcement之后这些东西就是我们接受的了，然后把它们加到前提集里去。在此基础上，研究怎么在S5系统里推出“你知道”，这个过程中就要用到推理别人知识的部分。
刘壮虎Q：（b1）从右到左是不需要的。
王彦晶A: 是的，通过T公理，再用必然化规则就可以得到。我们想强调的是，在S5系统里看似没有任何关于你知道我知道的规则，但是一个T公理加上必然化规则以后其实就得到了一个我是怎么知道别人知道什么的例子。
苏兴池Q：应用必然化规则时，对于不同的主体1，2，K1或K2都是可以随便加的吗？
王彦晶A：可以，必然化规则就是随便的模态词都可以往上加。从逻辑的角度看，K1或K2只是不同的模态词罢了。很多人觉得在知识的逻辑里必然化规则很奇怪，我怎么可能知道所有的重言式。但是如果没有必然化规则，在知识的逻辑中我们没有任何办法去推理别人的知识。看似反直观，但在特定条件下非常重要。
刘壮虎S：全信息的情况下可以用必然化规则。
邢滔滔S：在这个场景设定下，可以做这样的假设。
王彦晶S：（c1）为什么知道从右到左？我们需要假设每个孩子理性，不说谎。
王彦晶S：muddy children表面看上去关心的是自己知不知道自己是muddy children，但仔细看语形推理，其实是通过别人的知道不知道来推断自己的状态，这在语义分析中是看不出来的。
王彦晶Q：在你的证明中，有的前提并没有用到，比如b（3），所以是不是前提可以减弱？，
程莹莹A：是的，可以只有那个析取式。
王彦晶Q：什么是common knowledge？
程莹莹A：一个知识是所有人都知道的，并且所有人都知道所有人都知道这个知识，所有人都知道所有人都知道所有人都知道这个知识……无限嵌套下去。
王彦晶S：用语义解释时，许多模型一开始会假设有很多common knowledge。但在做语形推导的时候可以看到，其实并不需要common knowledge，假设可以弱很多。
赵晓玉Q：是不是只需要把那些东西作为一个前提假设条件就可以？
王彦晶A：不是。common knowledge的特点是无穷长的公式，这里想说的是真正做推理时只需要非常浅的层次，完全不需要common knowledge。
周北海Q： 逻辑学家说的common knowledge和平常大家说的不一样。平时说的不强调无穷。
王彦晶A：其实也需要。比如开车靠右行驶，必须是严格意义下的common knowledge。迎面来一辆车，虽然所有人事实上知道靠右行驶，但是对面的人不见得知道我知道靠右行驶，这样的话你并不觉得安全。
刘壮虎Q：社会公共知识需要common knowledge，但是我平时所说的知识，比如知道一个数学定理不需要假设这么强。
王彦晶A：对，common knowledge没有那么简单，隐含着大家都知道大家都知道。
邢滔滔S：基本上有多少人就需要有多少层，开会举手。
刘壮虎S：公共情景下，两层就够了；如果不是公共情景，就要无穷了。
王彦晶S: 公共情景下，几层跟人数有关。
刘壮虎Q：对于n个孩子的证明，实际上并不是归纳，每一个K都有对应的公理，并不是针对某一个K。在元逻辑中可能是归纳法，但在对象语言中不是归纳。
程莹莹A：是的。
周北海Q：奇迹是什么意思？没有奇迹是什么意思？
刘壮虎A：恒真的否定就是一个奇迹
周北海Q：可否用自然语言解释？
程莹莹A：需要再思考一下。
赵晓玉Q：布尔公式是指不出现任何模态算子的公式？
程莹莹A：是的。
邢滔滔Q：你的题目是要从语形上推断别人的知识，结论呢？
程莹莹A：从例子出发，加入必然化规则，它本身已经隐含在系统里，主要是把它突出出来。
邢滔滔Q：不是自己做一个新的系统？
程莹莹A：还是在原来的系统中。
邢滔滔Q：能不能在理论中证明，没有我提出的东西，系统内做不了这个东西?这个例子让我们在多大程度上推断别人的知识？推断别人的知识有没有更复杂的情况？
程莹莹A：刚开始从简单例子出发，以后会更深入。
苏兴池Q：用PAL刻画的优势在哪？PAL不是可以归约到EL？
程莹莹A：是的。
苏兴池Q：PAN系统有什么优势呢？
程莹莹A：王老师的出发点是提出一个算子为什么要归约回去？那提出一个算子还有什么意义？所以建立一个系统不需要归约。而且这个系统是完全的，之前的PAL系统是不完全的。
郑植Q：解释一下什么是公开宣告？
程莹莹A：从系统外部进入的，比如父亲说“明天要考试”，这就是公开宣告。但是公开宣告后不一定就知道，可能没听到，或者。。。
刘壮虎S：我宣告一个“布尔公式”以后就知道。不能宣告知识，只能宣告事实。我宣告一个事实，就能变成你的知识；我宣告一个知识，并不能变成你的知识。
程莹莹A：我觉得可以宣告知识，我宣告“张三知道……”
刘壮虎Q：你的系统中怎么推出别人知道的事情？
程莹莹A：没有新的系统。只是之前的系统中都没有明确的规则，所以我们给出了一个规则和公理，多主体的必然化规则，以及“宣告以后就全成为你们的知识”这个公理。
刘壮虎Q：我觉得“宣告以后就全成为你们的知识”，这个公理是关键。
周北海Q：这个还不太像我推断别人知道什么，应该是Ki要推断Kj知道什么。你讨论了公开宣告的细节，宣告了可能不知道，我宣布了你不一定明知，还需要证明。你承认必然化规则，那么你怎么回答“逻辑有效的东西你都知道”这个问题？
程莹莹A：我们谈的是在具体情况中，
周北海Q：但是必然化规则一用就必须面对逻辑全能问题。能不能有一个规则，既能保证你的要求，又能避免逻辑全能问题。
程莹莹A：还需要进一步研究。
赵晓玉Q：PAL里加的公理为什么只要求3是布尔的，其他要求不可以吗？
程莹莹A：其他情况很复杂，会有反例，需要进一步考虑。
程莹莹同学的这次报告主要是在知识逻辑的证明系统内通过语形的推导来阐明我们是如何推断别人的知识的。报告整体思路非常清晰，先概述了研究动机，然后利用muddy children的例子，分别在EL和PAL中进行语形推导，找出了相应的公理和规则。这种从一个小例子入手来研究问题的方法也很好。
我认为有待改进的地方有：
报告和研究不同，研究要深入，报告要尽量通俗易懂。由于本报告中有大量语形推演部分，为了听众理解，应该多给一些直观解释；其次，类似common knowledge这种大家并不是很熟悉的概念应该在使用之前给出定义。
你文中说要在知识的逻辑的证明系统内研究如何推断别人的知识。但这里只选取了EL和PAL，我觉得需要解释一下为什么选这两个系统？有什么好处？有没有有其他系统可以研究?
报告中引发大家兴趣的点不少，比如common knowledge，PAL，PAN，感觉有些削弱主线，应该再强调一下报告的主线，得出的结论。
注意时间控制。
王强是第一次点评，还不错，很认真，谈到了报告时的状况，不是提前准备好念一念的。
程莹莹也是第一次做报告，语言流畅，很不错。报告内容很丰富，注意主次分配好，最后要有个总结。其次注意一点，当你站在台上时，你就是主讲人，有很大的权力，可以适时中止大家的讨论，对于大家提出的问题也可以选择稍后回答，要注意控制报告时间。大家都要多往台上站，这是一种锻炼。讨论班的目的就是要锻炼大家，希望我们培养出来的学生有三个能力：能想，能写，能说。站台上能说，坐台下也要能说。博士生带头，硕士生也不能消极。我们再找时间专门讨论一下，如何积极参与学术交流。
reasoning20151103.pdf