王浩算法
节
3.3
所建立的公理系统对定理的证明,明显地依赖于人的经验、技巧,这就难于机械化。下面介绍的公理系统,对定理的证明给出了算法,便于利用计算机来实现定理的证明,也称定理证明自动化系统,这是1959年王浩提出的。
一、定理证明自动化系统
1.初始符号
2.形成规则
3.定义
4.公理
5.变形(推理)规则
6.定理的推演