Lambda the Ultimate

Wirth, Siekmann, Benzmueller & Autexier. Lectures on Jacques Herbrand as a Logician. SEKI Report SR-2009-01.

Herbrand's work, more than that of any other, provides the intellectual foundations of logic programming. This very readable article discusses Herbrands' contributions to proof theory and the formulation of the idea of a recursive function, and most importantly to PL, his fundamental theorem that yields a semi-decision algorithm for first-order logic and his unification algorithm.