Logic Theorist is a program written in 1956 by Herbert Simon, among others, that some people regard as the first AI program (it feels to me like the first proof assistant).