报告一：整合进程代数以及认知逻辑

2011年4月26日下午，应逻辑、语言与认知中心邀请，来自戴尔福特技术大学（Delft University of Technology）的Francien Dechesne博士在北京大学三教101室作了题为《 In Processes, We Believe - On Marrying Process Algebra and Epistemic Logic》的学术讲座。参加讲座的包括北京大学以及清华大学逻辑学专业的师生们。
在本次讲座中，Dechesne博士介绍了她与合作者的晚近工作：将进程代数（Process Algebra）与认知逻辑（Epistemic Logic）进行整合。进程代数在传统上最适合处理计算机多进程之间的通信与并发运行，认知逻辑则是处理知识与信念推理的逻辑，二者各有侧重，有各自的应用领域。而在安全协议验证这个具体应用中，我们既要需要处理进程的时序演进以及通信还需要用认知逻辑来直观的表述安全协议所要满足的特殊性质。一个很自然的想法就是要设计一种统一的理论框架，使得这二者各自的优势能够被结合在一起用来检验安全协议。
Dechesne博士在讲座中介绍了把这两种理论进行整合的一种办法。一个基本思想是在进程代数的语言中引入行动的主体可观测集（只有这个集合里的主体才能观察到特定的动作），然后通过某种结构操作语义（Structural Operational Semantics）在进程代数的模型中依据主体的观察不完全性生成用来解释认知逻辑的认知不可区分关系。总体来讲，这个工作给出了用认知模型解释的认知进程代数，以及用来推理认知及时态信息的一种认知时态逻辑，并且将这种新的认知时态逻辑与传统解释系统（Interpreted Systems）上的时态认知逻辑进行了初步的对比。而模型检测这种认知时态逻辑的算法复杂性问题，这个理论框架与其他理论框架间的关系问题，以及这个认知进程代数本身的理论问题将是下一步的研究重点。
Dechesne博士举了Dinning Cryptographers匿名协议的例子来演示了这个新的进程代数是如何工作的，之后又讨论了最新的进展，这使得本次讲座深入浅出。讲座结束后，王彦晶老师对这次讲座的内容作了概括以及评论。这次讲座进行的十分成功，主讲者与听众交流频繁，对相关的逻辑问题进行了热烈的探讨。

报告二：逻辑与博弈

2011年4月28日上午Dechesne博士在北大四教404室又做了一次题为《Playing Around Logic》的综述性报告。在这次报告中介绍了博弈（游戏）与逻辑的两种关系：博弈可以用来解释逻辑概念，而逻辑则可以用来研究博弈。前者的经典代表是一阶逻辑的博弈语义（赋值游戏），后者包括博弈逻辑与合作逻辑。Dechesne博士结合自己对于独立友好逻辑（IF Logic）的研究，对上述内容进行了较为细致的讲解。特别的，独立友好逻辑的博弈语义与一阶逻辑的博弈语义不同，是基于非完美信息博弈的，可以被翻译为存在形式的二阶逻辑，具有不同于一阶逻辑的特殊性质。课后，在座的北大、清华的学生与老师与Dechesne博士进行了气氛热烈的交流。

王彦晶