课程内容 课程内容 围绕学科理论体系中的模型理论，程序理论和计算理论 1.模型理论关心的问题 给定模型M,哪些问题可以由模型M解决；如何 比较模型的表达能力 本次讲座基于中学的等式 2.程序理论关心的问题 推理，与这些内容关系不大 给定模型M,如何用模型M解袂问题 包括程序设计范型、程序设计语言、程序设计、 形式语义、类型论、程序验证、程序分析等 3.计算理论关心的问题 给定模型M和一类问题，解决该类问题需多少资源
课 程 内 容 • 课程内容 围绕学科理论体系中的模型理论, 程序理论和计算理论 1. 模型理论关心的问题 给定模型M，哪些问题可以由模型M解决；如何 比较模型的表达能力 2. 程序理论关心的问题 – 给定模型M，如何用模型M解决问题 – 包括程序设计范型、程序设计语言、程序设计、 形式语义、类型论、程序验证、程序分析等 3. 计算理论关心的问题 给定模型M和一类问题, 解决该类问题需多少资源 本次讲座基于中学的等式 推理,与这些内容关系不大 2
课程内容 本讲座内容 以代数等式理论中的定理证明为例，介绍怎样从 中学生熟知的等式演算方法，构造等式定理的自 动证明系统，即将问题变为可用计算机求解 有助于理解计算思维的含义 计算思维（译文) 运用计算机科学的基础概念进行问题求解、系统 设计、以及人类行为理解等涵盖计算机科学之广度 的一系列思维活动
课 程 内 容 • 本讲座内容 – 以代数等式理论中的定理证明为例，介绍怎样从 中学生熟知的等式演算方法，构造等式定理的自 动证明系统，即将问题变为可用计算机求解 – 有助于理解计算思维的含义 计算思维（译文） 运用计算机科学的基础概念进行问题求解、系统 设计、以及人类行为理解等涵盖计算机科学之广度 的一系列思维活动 3
讲座提纲 ,基本知识 -代数项、代数等式、演绎推理规则、代数等式理 论、等式定理证明方法 项重写系统 -终止性、良基关系、合流性、局部合流性、关键 对 良基归纳法 -仅举例说明 Knuth-Bendix完备化过程 也仅举例说明
讲 座 提 纲 • 基本知识 – 代数项、代数等式、演绎推理规则、代数等式理 论、等式定理证明方法 • 项重写系统 – 终止性、良基关系、合流性、局部合流性、关键 对 • 良基归纳法 – 仅举例说明 • Knuth-Bendix完备化过程 – 也仅举例说明 4
基本知识 ·代数项和代数等式（仅涉及一个类型） -代数项 例：自然数类型nat 021,2,…:nat 常量 x,y:nat 变量 +,f:nat×nat→nat 二元函数 S:nat→nat 一元的后继函数 0,x,x+1,x+Sy)和100，y) 都是代数项 代数等式 例：x+0=x,x+S0y)=Sx+y) 5 x十y=z+5
基 本 知 识 • 代数项和代数等式（仅涉及一个类型） – 代数项 例：自然数类型nat 0, 1, 2, … : nat 常量 x, y : nat 变量 +, f : nat nat → nat 二元函数 S : nat → nat 一元的后继函数 0, x, x + 1, x + S(y)和f(100, y) 都是代数项 – 代数等式 例： x + 0 = x，x + S(y) = S(x + y) x + y = z + 5 5
基本知识 ·代数项和代数等式（涉及多个类型） 例：定义有限表：同类数据的有限序列的集合 6,17,50,28,188,92,30,67,15 18.8,9.2,50,77,8.6,5.5240.0 a,b,C,d,e,f,...Z (非数值数据》 上述数据涉及两个类型 。序列中元素的类型一 数值或非数值类型 ,这些序列所属的类型，称为表 (ist)类型 非数值类型 中学所学的代数概念在此已经扩展
基 本 知 识 • 代数项和代数等式（涉及多个类型） – 例：定义有限表：同类数据的有限序列的集合 • 6, 17, 50, 28, 188, 92, 30, 67, 15 • 18.8, 9.2, 50, 77, 8.6, 5.5, 40.0 • a, b, c, d, e, f, …, z （非数值数据） – 上述数据涉及两个类型 • 序列中元素的类型 — 数值或非数值类型 • 这些序列所属的类型，称为表（list）类型 — 非数值类型 – 中学所学的代数概念在此已经扩展 6