王浩算法

  节3.3所建立的公理系统对定理的证明,明显地依赖于人的经验、技巧,这就难于机械化。下面介绍的公理系统,对定理的证明给出了算法,便于利用计算机来实现定理的证明,也称定理证明自动化系统,这是1959年王浩提出的。

一、定理证明自动化系统

  1.初始符号
  2.形成规则
  3.定义
  4.公理
  5.变形(推理)规则
  6.定理的推演