A AUTOMATIC THEOREM PROVING SYSTEM BASED ON GENERALIZED RESOLUTION
基于广义归结的定理机器证明系统

The authors prove 350 theorems of "Principia Mathematica" by a theorem proving system based on generalized resolution. Compared it with traditional resolution,they complement new strategy, avoid self-resolution, and discuss its time and space complexity.