Donald W. Loveland
Donald W. Loveland researches automated reasoning and theorem proving. His shared 1962 paper with Martin Davis and George Logemann preceded his 1964 NYU doctorate. He developed model elimination and contributed to later implementations and logical proof methods. He joined Duke in 1973 and published a book on theorem proving in 1978. AAAI elected him a Fellow in 1993, and he received the Herbrand Award in 2001. His later book Three Views of Logic has shared authorship.
- Now at
- University of Michigan
- Works
- 85
- Citations
- 5,599
- h-index
- 24
Publication numbers from OpenAlex, as of 14 October 2026.
Timeline
-
1962–1964
Early proof algorithms and doctoral study
Loveland coauthored the 1962 paper A Machine Program for Theorem-Proving with Martin Davis and George Logemann. He earned his NYU doctorate in 1964.
-
1968–1974
Model elimination
Loveland published a 1968 paper on mechanical theorem proving by model elimination and later combined it with resolution. Loveland coauthored a 1974 implementation paper with S. Fleisig, A. Smiley and D. Yarmush.
-
1973–1978
Duke and an account of theorem proving
After academic appointments at NYU and Carnegie Mellon, Loveland joined Duke as a professor in 1973. He published Automated Theorem Proving: A Logical Basis in 1978. He chaired the department in several periods and remained a professor until 2001.
-
1993–2014
Recognition and wider views of logic
AAAI elected Loveland a Fellow in 1993, and he received the Herbrand Award in 2001. In 2014 he coauthored Three Views of Logic with Richard Hodel and Susan Sterrett. The book connects mathematical, philosophical and computing perspectives.
Sources and credits
Photo: users.cs.duke.edu; creator not stated. License: Not stated by source. Source: users.cs.duke.edu. Cropped to a square and resized. Ask us to remove or replace this photo.