Theorem proving
AI milestones in theorem proving, part of mathematics.
2 milestones
James Slagle Completes SAINT: A Symbolic Automatic Integrator
In 1961, James R. Slagle at MIT completed SAINT (Symbolic Automatic INTegrator), a heuristic program that solved indefinite integration problems at the level of a first-year calculus student, demonstrating that symbolic mathematical reasoning could be encoded in a computer program.
The Logic Theorist: first automatic theorem-proving program, developed by Newell, Shaw, and Simon
In late 1955, Allen Newell, J. Clifford Shaw, and Herbert A. Simon at RAND Corporation and Carnegie Institute of Technology completed the Logic Theorist, a computer program that proved mathematical theorems from Whitehead and Russell's Principia Mathematica by heuristic search, establishing that symbolic reasoning could be mechanised.