1953年，美国乔治敦大学组织了第一次机器翻译的实际实验。 　　1954年7月，IBM公司在701计算机上做了俄译英的公开表演。 　　1956年，Newell(艾伦.纽厄尔)和Simon(西蒙)等人首先取得突破，他们编的程序Logic Theorist(应用启发式技术)证明了《数学原理》第二章中的三十八条定理，又于1963年证明了该章中的全部五十二条定理，走上了以计算机程序来模拟人类思维的道路，第一次把求解方法和问题的领域知识分离开。 　　1958年定理证明方面取得新成就，美籍数理逻辑学家王浩在IBM704计算机上以3-5分钟证明了《数学原理》有关命题演算的全部220条定理，还用了几分钟证明了该书中带等式的谓词演算的150条定理中的85%，1959年再接再厉，仅用了8.4分钟就证明了以上全部定理。 　　1959年，IBM公司的Gelernter(格伦特尔)研制出平面几何证明程序。