Textbook of AI

1929–2015, Physicist, AI researcher at IBM

Herbert Gelernter was an American physicist and AI researcher at IBM who developed the Geometry Theorem Prover (1958–1959), one of the earliest AI programs and the first to prove non-trivial theorems of Euclidean geometry by combining symbolic search with a "diagram" , a numerical model of a particular instance, used to prune the search space. The use of a semantic model to guide a syntactic search was a novel idea and an ancestor of modern model-driven theorem proving.

Gelernter contributed to early list-processing language design (FLPL, an extension of FORTRAN with list-processing primitives, predated by McCarthy's LISP but partly inspiring it) and later moved to academia, spending much of his career at SUNY Stony Brook on machine learning and chemical informatics, including the SYNCHEM program for synthesis-route planning in organic chemistry.