The Wikipedia article details the Logic Theorist, created in 1956 by Allen Newell, Herbert A. Simon, and Cliff Shaw. Widely considered the first AI program, it successfully proved 38 of the first 52 theorems in Principia Mathematica, even discovering more elegant proofs than those originally crafted by Russell and Whitehead.
Jeff Shrager has reanimated LT in IPL-V with a new implementation.
