Donald W. Loveland

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]

Donald W. Loveland
Born	(1934-12-26) December 26, 1934 (age 90) Rochester, New York
Alma mater	New York University
Known for	DPLL algorithm
Awards	Herbrand Award 2001
Scientific career
Fields	Computer science
Institutions	Duke University
Thesis	Recursively Random Sequences  (1964)
Doctoral advisors	Peter Ungar, Martin David Davis
Doctoral students	Owen Astrachan, Susan Gerhart

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]

Bibliography

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. January 26, 2014. ISBN 978-1-4008-4875-1.

Selected papers

• Davis, Martin; Logemann, George; Loveland, Donald (July 1, 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. (April 1, 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. (April 1, 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. (January 1, 1974). "An Implementation of the Model Elimination Proof Procedure". Journal of the ACM. 21 (1): 124–139. doi:10.1145/321796.321807. S2CID 15686713.

See also

• Model elimination