Donald W. Loveland (born December 26, 1934, in Rochester, New York)^[1] is a professor emeritus of computer science at Duke University who specializes in artificial intelligence.^[2] He is well known for the Davis–Putnam–Logemann–Loveland algorithm.^[3]

Loveland graduated from Oberlin College in 1956, received a master's degree from the Massachusetts Institute of Technology in 1958 and a Ph.D. from New York University in 1964. He joined the Duke University Computer Science Department in 1973. He previously served as a faculty member in the Department of Mathematics at New York University and Carnegie Mellon University.^[1][4][5]

He received the Herbrand Award for Distinguished Contributions to Automated Reasoning in 2001.^[5] He is a Fellow of the Association for Computing Machinery (2000),^[6] a Fellow of the Association of Artificial Intelligence (1993),^[7] and a Fellow of the American Association for the Advancement of Science (2019).^[8]

Books

• Automated Theorem Proving: A Logical Basis. North-Holland Publishing Company. 1978. doi:10.1016/c2009-0-12705-8. hdl:2445/109943. ISBN 978-0-7204-2500-0.
• 6th Conference on Automated Deduction. Lecture Notes in Computer Science. Vol. 138. (Editor) Springer-Verlag, London. 1982. doi:10.1007/BFb0000048. ISBN 978-3-540-11558-8. S2CID 33583364.
• Automated Theorem Proving: After 25 Years. Contemporary Mathematics. Vol. 29. (with W.W. Bledsoe) American Mathematical Soc. 1984. doi:10.1090/conm/029. ISBN 978-0-8218-5027-5.
• Three Views of Logic: Mathematics, Philosophy, and Computer Science. (with R. Hodel and S.G. Sterrett) Princeton University Press. 26 January 2014. ISBN 978-1-4008-4875-1.

Selected papers

• Davis, Martin; Logemann, George; Loveland, Donald (1 July 1962). "A machine program for theorem-proving". Communications of the ACM. 5 (7): 394–397. doi:10.1145/368273.368557. hdl:2027/mdp.39015095248095. S2CID 15866917.
• Loveland, Donald (1966). "A New Interpretation of the von Mises' Concept of Random Sequence". Zeitschrift für Mathematische Logik und Grundlagen der Mathematik. 12 (1): 279–294. doi:10.1002/malq.19660120124.
• Loveland, Donald W. (1 April 1968). "Mechanical Theorem-Proving by Model Elimination". Journal of the ACM. 15 (2): 236–251. doi:10.1145/321450.321456. S2CID 18377884.
• Loveland, D. W. (1969). "A Simplified Format for the Model Elimination Theorem-Proving Procedure". Automation of Reasoning. pp. 233–248. CiteSeerX 10.1.1.1017.8248. doi:10.1007/978-3-642-81955-1_14. ISBN 978-3-642-81957-5.
• Loveland, D.W. (December 1969). "A variant of the Kolmogorov concept of complexity". Information and Control. 15 (6): 510–526. doi:10.1016/S0019-9958(69)90538-5.
• Loveland, D. W. (1970). "A linear format for resolution". Symposium on Automatic Demonstration. Lecture Notes in Mathematics. Vol. 125. pp. 147–162. doi:10.1007/BFb0060630. ISBN 978-3-540-04914-2. ISSN 0075-8434. S2CID 121021241.
• Loveland, D. W. (1 April 1972). "A Unifying View of Some Linear Herbrand Procedures". Journal of the ACM. 19 (2): 366–384. doi:10.1145/321694.321706. S2CID 14244283.
• Fleisig, S.; Loveland, D.; Smiley, A. K.; Yarmush, D. L. (1 January 1974). "An Implementation of the Model Elimination Proof Procedure". Journal of the ACM. 21 (1): 124–139. doi:10.1145/321796.321807. S2CID 15686713.

• Model elimination