文档介绍：代数等式理论的自动定理证明 计算机科学导论第一讲
计算机科学技术学院
陈意云
0551-63607043
******@ustc.
课程内容
课程内容
围绕学科理论体系中的模型理论, 程序理论和计算理论
1. 模型理论关心的问题
给定模型M,哪些问题可以由模型M解决;如何比较模型的表达能力
2. 程序理论关心的问题
给定模型M,如何用模型M解决问题
包括程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等
3. 计算理论关心的问题
给定模型M和一类问题, 解决该类问题需多少资源
本次讲座与这些内容关系不大
课程内容
本讲座内容
以代数等式理论中的定理证明为例,介绍怎样从中学生熟知的等式演算方法,构造自动定理证明系统,即将问题变为可用计算机求解
有助于理解什么是计算思维
计算思维(译文)
运用计算机科学的基础概念进行问题求解、系统设计、以及人类行为理解等涵盖计算机科学之广度的一系列思维活动
讲座提纲
基本知识
代数项、代数等式、演绎推理规则、代数等式理论、等式定理证明方法
项重写系统
终止性、良基关系、合流性、局部合流性、关键对
良基归纳法
Knuth-Bendix完备化过程
基本知识
代数项
仅涉及一个类型的代数项
例:自然数类型的项0, x, x + 1, x + S(y), f(100, y)
其中x和y变量,f 和S是一阶函数,S是后继函数
涉及多个类型的代数项
若有变量 x : atom, l : list(list是atom的表类型)
并有函数 nil : list, cons : atom list list
first : list atom,rest : list list
则 nil, cons(x, l), rest(cons(x, nil)), rest(cons(x, l))和cons(first(l), rest(l))都是代数项
基本知识
代数等式
例: x + 0 = x,x + S(y) = S(x + y), x + y = z + 5
first(cons(x, l)) = x [x : atom, l : list]
rest(cons(x, l)) = l [x : atom, l : list]
其中方括号中至少列出等式中出现的变量
等式证明
例:基于一组等式:x + 0 = x和x + S(y) = S(x + y)
怎么证明等式x + S(S(y)) = S(S(x + y)) ?
需要有推理规则
等式证明的演绎推理规则
自反公理:M M 对称规则:
传递规则:
加变量规则:
等价代换规则:
M = N
N = M
M = N N = P
M = P
M = N
M = N , x : s
M = N , x : s P = Q
P/xM = Q/xN
基本知识
x不在中
P , Q 是类型s的项
等式推理的例子
等价代换规则:
等式公理:x + 0 = x和x + S(y) = S(x + y)
证明等式: x + S(S(y)) = S(S(x + y))
证: x + S(S(y)) 根据x + S(z) = S(x + z),S(y) = S(y)
= S(x + S(y)) 使用等价代换规则得到第一个等式
= S(S(x + y)) 根据S(z) = S(z), x + S(y) = S(x + y)
使用等价代换规则得到第二个等式
再利用传递规则可得要证的等式
M = N , x : s P = Q
P/xM = Q/xN
基本知识
基本知识
代数等式理论(algebraic equation theory)
在项集T 上从一组等式E(公理、公式)能推出的所
有等式的集合称为一个等式理论(通俗的解释)
代数等式理论的定理证明
判断等式 M = N []是否在某个代数等式理论中
常用证明方法
把M和N分别化简, 若它们的最简形式一样则相等
分别证明M和N都等于L
证明MN等于0
还有其它方法
基本知识
哪种证明方法最适合于计算机自动证明?
把M和N分别化简, 若它们的最简形式一样则相等
若基于所给的等式E,能把M和N化简到最简形式,则这种方式相对简单,便于自动证明
分别证明M和N都等于L
自动选择L是非常困难的
证明MN等于0
不适用于非数值类型的项,例如先前给出的atom类型的表