定理机器证明与吴文俊方法

Theorem Proving by Machine and Wu Wenjun’s Principle

作为人类脑力的一种延伸,数学机械化和定理机器证明研究的学术努力及其每一个重大突破,都必将对人类和科学产生意义深远的冲击。

In the late of 1970s,Prof.Wu Wenjun created a new theory for theorem proving by machine.Based on Wu's method,more than 600 geometric theorems have been proved by computer.Wu's method is not only a breakthrough in theorem proved by machine,but also initiates a series of researches,such as automatic derivation of unknown relation,nonlinear programming and robotics,etc.