Donald W. Loveland
American mathematician (born 1934)
From Wikipedia, the free encyclopedia
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 | December 26, 1934 |
| 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) |
| Peter Ungar, Martin David Davis | |
Doctoral students | |
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.
