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