模态不动点逻辑
Yde Venema （http://staff.science.uva.nl/~yde/)
阿姆斯特丹大学逻辑，语言与计算研究所

一、讲座主题介绍及每次讲座内容题目与要点：
模模态不动点逻辑 (>>Workshop Modal Fixpoint Logics)
模态不动点逻辑构成了相当有意思的一个研究领域。这首先是由于它们在广泛的学科——从哲学、经济学到计算机科学——当中有重要的应用。作为例子，我们提到了研究多主体间的公共知识的认知逻辑，以及在软件的描述与检测理论中使用的线性时序逻辑和计算树形逻辑。模态不动点逻辑重要的原因之二是，它们的极为丰富的逻辑与数学理论刻画了各不相同的领域之间深层次的联系，包括格论、自动推理理论以及泛余代数理论。
这一（短期）课程将概述模态不动点逻辑理论，重点讲述模态mu演算。这是最为一般的系统——所有有名的模态不动点逻辑都可被视为模态mu演算的一个片断。课程将讨论模态mu演算的一些最重要的结果，特别是要分析它的博弈理论以及代数方面的性质。
本课程的另一个重要部分是展示模态不动点逻辑和自动推理理论间的联系。
下面是6×2小时课程的内容概要：
1、模态不动点逻辑引论
（1）基本定义与例子
（2）将要引出的问题
2、模态mu-演算
（1）语法
（2）博弈论语义
3、模态不动点逻辑的代数理论
（1）Knaster-Tarski定理
（2）不动点的逼近及其构造性
4、线性时序逻辑和无穷字上的自动推理
主要是详细讨论一个易接受而又非常重要的不动点逻辑
5、模态mu演算和树形自动推理
介绍一种重要的证明工具
6、有关模态mu演算的结果
讨论这个系统的最重要的一些性质

MODAL FIXPOINT LOGICS
Modal fixpoint logics constitute a research field of considerable interest. This is first of all because they have important applications in a wide range of disciplines, ranging from philosophy via economics to computer science. As examples we mention the epistemic logic of common knowledge between many agents, and the use of logics such as LTL (linear temporal logic) and CTL (computation tree logic) in the theory of specification and verification of software. A second reason for the importance of these logics is given by their rich logical/mathematical theory, which features deep connections with fields as diverse as lattice theory, automata theory, and universal coalgebra.
In the course we will give an overview of the theory of modal fixpoint logics. We will focus on the modal mu-calculus (muML), this being the most general system -- all well-known modal fixpoint logics can be seen as fragments of muML. We will discuss the most important results concerning muML, and in particular treat game-theoretic and algebraic aspects of it. An important part of the course will lie in exhibiting the connection between modal fixpoint logics and automata theory. The programme of the course, consisting of six two hour lectures, is the following.
1. Modal fixpoint logics: introduction
(basic definitions, examples, questions to be addressed)
2. The modal mu-calculus
(syntax, game-theoretical semantics)
3. Algebraic theory of modal fixpoint logics
(Knaster-Tarski theorem, approximations, constructiveness of fixpoints)
4. Linear temporal logic and automata on infinite words
(a detailed exposition of an easy but important modal fixpoint logic)
5. The modal mu-calculus and tree automata
(introducing a key proof tool)
6. Results on the modal mu-calculus
(a discussion of the most important properties of the system)
说明：以上六个题目及要点可能会有临时小的调整。

二、时间：6月16日-21日，每天上午9：30-12：00

三、地点：中国人民大学明德楼0104（明德楼位于人大西门旁，0104在明德楼的西面，属商学院）

四、讲座人简介：
Yde Venema博士是阿姆斯特丹大学逻辑、语言与计算研究所副教授。他于1992年以《多维模态逻辑》在该大学获得博士学位。Venema博士研究领域为模态逻辑理论，侧重于代数、余代数及博奕论。Venema博士是有名教材《模态逻辑》的作者之一，同时也是其他三本著作的合著者。他当前正主持研究项目“代数和余代数：模态代数的数学环境（情境）”。
Yde Venema is an associate professor at the Institute for Logic, Language and Computation of the University of Amsterdam. He received his PhD from the same university in 1992 with a dissertation entitled `Many-dimensional Modal Logic'. The research of Dr Venema concerns the theory of modal logic, with a focus on algebraic, coalgebraic and game-theoretic aspects. Dr Venema is a co-author of the well-known textbook `Modal Logic' and of three monographs, and he has published some thirty research papers in international journals. He is leading a research group `Algebra and Coalgebra: the mathematical environments of modal logic'.