人工智能中策略推理的模态逻辑70031

课程内容：

本课程的总体目标是发展在人工智能中使用模态逻辑进行知识表达和自动推理的知识和实践技能。

课程主题：

1、基本概念：模态语言；克里普克模型和框架；模态结果关系，决策问题，有效性；正规模态逻辑。

2、模型：不变性结果，相互模拟；标准翻译；表征和可定义性；模拟和安全。

3、框架：框架可定义性和二阶逻辑；可定义和不可定义的属性；有限框架；自动一阶对应。

4、系统推理：多智能体系统；逻辑在MAS中的作用；形式证明。

5、关于时间和变化的推理：时序逻辑；线性时序逻辑；计算树逻辑；模型检测时态逻辑的复杂性。

6、关于战略能力的推理：并发博弈结构；交替时间时序逻辑；代理、系统、博弈。

7、战略能力验证：交替时间时序逻辑的性质(有效性和可满足性问题)；模型检查ATL；模型检查ATL*。

8、不完全信息下的能力：策略和知识；不完全信息下ATL的性质(有效性和可满足性问题)；主观解释。

学习成果：

成功完成本课程后，学生将能够：

1、识别并展示对模态运算符独特特征的理解。

2、理解并回忆课程中提出的逻辑和逻辑系统的定义，以及主要证明的思想。

3、理解各种逻辑的差异，及其表达能力和局限性。

4、使用并发博弈结构的框架对多智能体系统(MAS)的具体实例进行建模。

5、能将MAS中agent策略能力的非正式规范(用英语表达)翻译成时间逻辑LTL和CTL公式，以及交替时序逻辑ATL公式。

6、认识到具有完全/不完全环境信息的智能体和其他智能体的建模差异，以及对过去事件具有完全/不完全回忆的智能体建模的差异。

7、能在并发博弈结构中应用支持ATL属性验证的模型检查算法。