Current as of:  January 2020

Donald W. Loveland


A.B., Oberlin College, 1956.

S.M., Massachusetts Institute of Technology, 1958.

Ph.D., New York University, 1964.


Mathematician Programmer, IBM, Yorktown Heights (1958-1959).

Research Assistant, New York University (1960-1961).

Instructor, New York University (1963-1964).

Assistant Professor, New York University (1964-1967).

Assistant Professor of Mathematics and Computer Science, Carnegie-Mellon University (1967-1969); Associate Professor (1969-1973).

Professor, Computer Science Department, Duke University (1973-2001).

Chairman, Computer Science Department, Duke University (1973-1978; 1991-1992; 1998-1999).

Professor Emeritus, Computer Science Department, Duke University (2001- ).


Fellow of the AAAS (elected 2019).

Herbrand Award--For Distinguished Contributions to Automated Reasoning (2001).

Fellow of the ACM (elected 1999).

Fellow of the American Association of Artificial Intelligence (elected 1993).

IBM Distinguished Faculty Visitor, IBM T.J. Watson Research Center, 9 mos. (1979-1980).

National Science Foundation Co-op Fellow, New York University (1961-1963).

Listed in Who's Who in America.

Sigma Xi


National Science Foundation, GP-5273, October 1965-January 1967 (with M. Davis).

NSF, GP-7064, April 1967-April 1969 (with M. Davis) (consultant only after September 1967 as required by my move to Carnegie-Mellon University).

NSF, GJ-580, July 1969-June 1971 (with P. Andrews).

NSF, GJ-28457X, July 1971-June 1976 (with P. Andrews) (terminated association with grant after August 1973 as required by my move to Duke University).

NSF, DCR-75-00666, July 1975-June 1977.

Air Force Office of Scientific Research, AFOSR-81-0221, July 1981-June 1983 (with B. Ballard, A. Biermann, R. Wagner).

AFOSR, AFOSR-83-0205, July 1983-June 1986 (with B. Ballard, A. Biermann, R. Wagner).

Army Research Office, DAAG29-84-K-0072, May 1984-September 1987 (with A. Biermann).

ARO, DAAL03-88-K-0082, July 1988-June 1991 (with A. Biermann).

NSF, IRI-88-05696, Aug. 1988-July 1989 (with G. Nadathur).

NSF, CCR-8900383, Oct. 1989-March 1992.

NSF, CCR-9116203, Feb. 1992-Feb. 1996.

CISE Institutional Infrastructure Program (PI, as Dept. Chair; 4 Co-PIs). Awarded April, 1992. (Approx. $1.4 million.) For purchase and partial support of Thinking Machines CM-5 and support equipment.

NSF, CCR-9625544, Jan. 1996-Dec. 1996. Funding for the Workshop on Future Directions of Automated Deduction.

NSF INT-9514375, July 1996-June 1998 (with Owen Astrachan). U.S. -- Germany cooperative research travel grant.



Automated Theorem Proving: A Logical Basis. North-Holland, Amsterdam, 1978, xiii + 405.

6th Conference on Automated Deduction (Editor). Springer-Verlag, Berlin, 1982, viii + 389.

Automated Theorem Proving: After 25 Years (Editor, with W.W. Bledsoe). Contemporary Mathematics, Vol. 29, Amer. Math. Soc., Providence, 1984, ix + 360 pp.

Three Views of Logic: Mathematics, Philosophy, and Computer Science. With coauthors Richard E. Hodel and S. G. Sterrett. Princeton University Press, Princeton, NJ, 2014, xv+322 pp.


A near-Horn Prolog for compilation, (with D. Reed). Computational Logic: Essays in Honor of Alan Robinson (Lassez and Plotkin, eds.), The MIT Press, Cambridge, MA (1991), 542-564.

METEORs: high performance theorem provers for Model Elimination, (with O.L. Astrachan). Automated Reasoning: Essays in Honor of Woody Bledsoe, R.S. Boyer ed., Kluwer Academic Publ., Dordrecht (1991).

Proof procedures for logic programming, (with G. Nadathur). Handbook of Logic in Artificial Intelligence and Logic Programming (Gabbay, Hogger and Robinson, eds.), Vol. 5, Clarendon Press, Oxford (1997), 163-234.

DPLL: The core of modern satisfiability solvers (with A. Sabharwal and B. Selman). Martin Davis on Computability, Computational Logic, and Mathematical Foundations (Omodeo and Policriti, eds.), Outstanding Contributions to Logic (Vol. 10), Springer-Verlag, Heidelberg (2016), 315-335.


A machine program for theorem-proving, (with M. Davis and G. Logemann). Communications of the Association for Computing Machinery, 5 (1962), 394 - 397.

A new interpretation of the von Mises' concept of random sequence. Zeit. fur Math. Logik and Grundlagen der Mathematik, 12 (1966), 279 - 294.

The Kleene hierarchy classification of recursively random sequences. Transactions of the American Mathematical Society, 125 (1966), 497 - 510.

Mechanical theorem-proving by Model Elimination. Journal of the Association for Computing Machinery, 15 (2) (1968), 236 - 251.

A simplified format for the Model Elimination theorem-proving procedure. Journal of the Association for Computing Machinery, 16 (1969) 349 - 363.

Theorem-provers combining Model Elimination and Resolution. Machine Intelligence 4, Edinburgh University Press (1969), 73 - 86.

A variant of the Kolmogorov concept of complexity. Information and Control 15 (1969), 510 - 526.

A linear format for resolution. Lecture Notes in Mathematics 125, Springer-Verlag, Berlin (1970), 147 - 162.

A brief primer on resolution proof procedures. Computer Science Research Review 1970 - 71, Carnegie-Mellon University (September, 1971), 7 - 19.

A unifying view of some linear herbrand procedures. Journal of the Association of Computing Machinery, 19 (1972), 366 - 384.

An implementation of the Model Elimination proof procedure, (with S. Fleisig, A. Smiley, and D. Yarmush). Journal of the Association of Computing Machinery, 21(1974), 124 - 139.

Mathematical computer science courses: a position paper. SIGCSE Bulletin 6, 3 (September 1974) 106 - 108.

The heart of computer science, (Co-authors: N. Gibbs, J. Ortega). SIGCSE Bulletin 6, 4 (Dec. 1974) 13-14.

Deleting repeated goals in the extended problem reduction format. (with C.R. Reddy). Journal of the Association of Computing Machinery, 28 (4) (1981), 646-661.

Performance bounds for binary testing with arbitrary weights. Acta Informatica 22 (1985), 101-114.

Finding test-and-treatment procedures using parallel computation, (with Duval, Wagner, Han; fourth author). Jour. of Parallel and Distr. Computing 4, (1987), 309-318.

Finding critical sets. Journal of Algorithms 8, 3 (Sept. 1987), 362-371.

Completeness. Encyclopedia of Artificial Intelligence, John Wiley and Sons (1987).

Near-Horn Prolog and beyond. Jour. of Auto. Reasoning, 7, 1 (1991), 1-26.

A comparison of three prolog extensions, (with D. Reed). Jour. of Logic Programming 12 (1992), 25-50

On the complexity of belief network synthesis and refinement, (with M. Valtorta). International Jour. of Approximate Reasoning 7 (1992), 121- 148.

Satchmore: Satchmo with Relevancy, (with D.W. Reed and D.S. Wilson). Journal of Automated Reasoning 14 (1995), 325-351.

Near-Horn Prolog and the ancestry family of procedures, (with D. Reed). Annals of Math. and Artif. Intell. 14 (1995), 225-249.

The use of lemmas in the Model Elimination procedure, (with O. Astrachan). Journal of Automated Reasoning 19 (1997), 117-141.

Automated Deduction: looking ahead. AI Magazine 20, 1 (Spring 1999), 77-98.

Automated Deduction: some achievements and future directions. Communications of the ACM, 43 (11ex: Virtual Extension Edition)(2000), paper #10.

Satchmorebid: Satchmore(Re) with bidirectional relevancy (with A. H. Yahya). New Generation Computing, 21, 3, (2003), 177-207.

Mark Stickel: his earliest work. Journal of Auto Reasoning, 56,2 (2016), 99-112. 


Empirical explorations of the Geometry Theorem Machine, (with H. Gelernter and J.R. Hansen). Proc. of the Eastern Joint Comp. Conference, 17 (1960), 143 - 147. Reprinted in Computers and Thought (Feigenbaum and Feldman, eds.) McGraw-Hill (1963).

On minimal-program complexity measures. Conference Record of the ACM Symposium on Theory of Computing (May, 1969), 61 - 65.

A hole in goal trees: some guidance from resolution theory. Proc. of the Third Int'l. Joint Conf. on Artificial Intelligence (August, 1973), 153 - 161 (with M. Stickel). Also in IEEE Trans. on Computing, C-25 (April, 1976), 335 - 341.

Presburger arithmetic with bounded quantifier alternation. Proc. of the ACM Symposium on the Theory of Computing (May, 1978), 320 - 325 (with C. Ramu Reddy).

Selecting optimal test procedures from incomplete test sets. First Int'l. Symposium on Policy Analysis and Information Systems, Duke University, (June 1979). (Paper in proceedings.)

Simplifying interpreted formulas, (with R. Shostak). Fifth Conference on Automated Deduction, Les Arcs, France (July 1980). (Proceedings published in series Lecture Notes in Computer Science 87, Springer-Verlag, (1980).)

A computerized consultation system on Alzheimer's disease (Fifth of eight authors). Second Annual Conf. of the Amer. Assoc. for Med. Systems and Informatics, Baltimore, (October 1983).

Detecting ambiguity: an example of knowledge evaluation, (with M. Valtorta). Proc. of the Eighth Int'l. Joint. Conf. on Artif. Intell., Karlsruhe, W. Germany, Aug. 1983. Reprinted in Validating and Verifying Knowledge- Based Systems, U.G. Gupta ed., IEEE Computer Society Press, Los Alamitos, CA (1991), 391 - 395.

The Graduate Course Adviser: a multi-phase rule-based expert system, (with M. Valtorta, B. Smith). IEEE Workshop on Principles of Knowledge- Based Systems, Denver (Dec. 1984).

Finding test-and-treatment procedures using parallel computation, (with Duval, Wagner, Han; fourth author). Short version given at 1986 Int'l. Conf. on Parallel Processing (Chicago, Aug. 1986). (Full paper listed under publications.)

Near-Horn Prolog. Proc. of the Fourth Int'l. Conf. on Logic Programming, Melbourne (May, 1987), 456-469.

A simple near-Horn Prolog interpreter, (with B. T. Smith). Proc. of the Fifth Int'l Conf. Symp. on Logic Programming, Seattle (August, 1988).

An alternative characterization of disjunctive logic programs, (with D. Reed and B.T. Smith). International Logic Programming Symposium '91, San Diego (October, 1991).

The near-Horn approach to disjunctive logic programming, (with D. Reed and B.T. Smith). Extensions of Logic Programming, Second International Workshop, ELP'91 (Stockholm), Lecture Notes in Artif. Intell. 596, Springer-Verlag, Heidelberg (1992), 345-369.

Uniform proofs and disjunctive logic programming, (with G. Nadathur). Proc. of the IEEE Symp. on Logic in Comp. Sci. (LICS-95), San Diego, June, 1995.


Automated Deduction: Some achievements and future directions. Report to the National Science Foundation, July 1997, iii+47pp. Purpose is to assess the status and research opportunities of the Automated Deduction field for the NSF. Based on a Workshop on the Future Directions of Automated Deduction, April 20-21, 1996. Chicago.

SERVICE (Partial Listing)


Chairman, Computer Science Department, 1973-1978, 1991-1992, 1998-1999.

Chairman, Faculty Recruiting Committee, Computer Science Dept., 1978-79, 1980-1981.

Director of Graduate Studies, Computer Science Dept., 1982-1985.


Chairman, Committee for prospective Jour. of Computational Logic, 1981- 1982. (Became Jour. of Automated Reasoning.)

Member of Subcommittee for Current ATP Prize, 1982. (Prize awarded at annual AMS meeting, Denver, Jan. 1983).

Member of Univ. of Pennsylvania AI Center Advisory Board, April 1991 - August 1995.

Organizer, Japanese-American Workshop on Automated Theorem Proving. Durham, NC, March 1994. Sponsors: ICOT(Japan), Duke University.

Trustee, CADE Inc., 1994-1997. (CADE Inc. is the corporation set up to oversee the Conference on Automated Deduction. This is the premier conference in the area of automated theorem proving.)

Co-organizer, Conference on Disjunctive Logic Programming and Databases: Nonmonotonic Aspects. Schloss Dagstuhl, Saarbrucken, Germany. July, 1996.

Organizer, Workshop on Future Directions of Automated Deduction. Chicago, April 1996. Sponsor: NSF.


Member of Editorial Board, Artificial Intelligence Jour., July 1983 - June 1992.

Guest Editor (with J. Lobo and A. Rajasekar), special volume on Disjunctive Logic Programming, Annals of Mathematics and Artificial Intelligence, Vol. 12, I-II, J.C. Baltzer AG, Amsterdam, 1994.

Member of Editorial Board, Journal of Automated Reasoning, September 1983 - 2001.

Managing Editor, book series SYMBOLIC COMPUTATION - ARTIFICIAL INTELLIGENCE (renamed ARTIFICIAL INTELLIGENCE, 1991), Springer-Verlag, January 1984 - August 1992. On board of editors until 2001.


Heuristics and analysis in inference systems, Panel on Heuristics, Learning and Control, Joint Automatic Control Conference, St. Louis, Mo., August 1971.

The state of automated deduction: a report on the Automatic Deduction Workshop 1977, Fifth Int'l. Joint Conf. on Artif. Intelligence, Cambridge, Mass., August 1977.

Automated theorem proving: a quarter-century review. Special Session on Auto. Thm. Proving, Amer. Math. Soc. Annual Mtg., Denver, CO., January 1983.

Knowledge acquisition and evaluation. Army Conf. on AI Applications to Battlefield Info. Systems, Silver Springs, Md., April 1983. Talk summary in Proc. of Artif. Intell. Conf.

Automated theorem proving: mapping logic into AI. Int'l. Sympos. on Methodologies for Intell. Systems. Knoxville, TN., Oct. 1986. Full talk appears in Proc. of the Int'l. Sympos. on Methodologies for Intell. Systems.

CS Symposium: Intelligent Systems (keynote talk), Columbia, SC, Mar. 1990.

Disjunctive Logic Programming: Prolog with Case Analysis. Logic Programming Conference '91( one of two invited papers), Tokyo, July 8-11, 1991. Note: This talk was also given in Kyoto(7/22) and Osaka(7/23).

The METEOR implementation of Model Elimination with lemmas. Frontiers in Computing Symposium. Austin, TX, Nov. 15-16, 1991. Also given as the invited paper at the Workshop on Non-Resolution Theorem Proving, Lautenbach, Germany, March 18-20, 1992.

Proof Procedures for Disjunctive Logic Programming. Workshop on Disjunctive Logic Programming and Disjunctive Databases (one of three keynote papers), 13th World Computer Congress IFIP'94, Hamburg, Germany, August, 1994.

When does a First-order Proof Procedure define a good Logic Programming Procedure? Workshop on Automated Theorem Proving (one of four invited papers), International Symposium on Fifth Generation Computer Systems 1994, Tokyo, Japan, December 13 - 16, 1994.


Program Committee Member, 4th Annual Symposium on Theory of Computing, Denver, May, l972.

Member of ACM Curriculum Committee on Computer Science, 1974-1976 (to review and update curriculum 1968 report).

Program Committee Member, 4th Workshop on Automatic Deduction, Austin, Texas, February, 1979.

Program Chairman, 6th Conference on Automated Deduction, New York, Spring 1982.

Program Committee Member, 7th Conference on Automated Deduction, Napa Valley, CA, Spring, 1984.

Program Committee Member, 10th Conference on Automated Deduction, Kaiserslautern, West Germany, July, 1990.

Co-Chairman, Workshop on Disjunctive Logic Programming, San Diego, CA, Nov. 1, 1991.(Held in conjunction with the International Logic Programming Symposium 1991.)

Program Committee member, 11th Conference on Automated Deduction, Saratoga Springs, NY, July, 1992.

Organizer, Japanese-American Workshop on Automated Theorem Proving, Durham, NC, March 1994. Sponsors: ICOT(Japan), Duke University.

Co-organizer, Conference on Disjunctive Logic Programming and Databases: Nonmonotonic Aspects. Schloss Dagstuhl, Saarbrucken, Germany. July, 1996.

Organizer, Workshop on Future Directions of Automated Deduction, Chicago, April 1996. Sponsor: NSF.


American Association of Artificial Intelligence.

Association for Computing Machinery.

Association of Symbolic Logic.

American Association for the Advancement of Science.


Robert Daley, Ph.D., Mathematics, 1971. Pseudo-Recursiveness and Pseudo-Randomness within Minimal Program Complexity Hierarchies.

Susan Gerhart, Ph.D., Computer Science, 1972. Verification of APL Programs.

C. Ramu Reddy, Ph.D., Computer Science, 1978. Automatic Theorem Proving: New Results on Goal Trees and Presburger Arithmetic.

M. Valtorta, A.M., Computer Science, 1983. The Graduate Course Adviser.

C. van der Veen, A.M., Computer Science, 1985. The Development of the Updater for TAME.

D.C. Mutchler, Ph.D., Computer Science, 1986. Search with Very Limited Resources.

P.J. Lanzkron, M.S., Cmputer Science, 1987. Results on the Test and Treatment Problem.

M. Valtorta, Ph.D., Computer Science, 1987. Automating Rule Strengths in Expert Systems.

D.W. Reed, M.S., Computer Science, 1988. Near-Horn Prolog: a First-order Extension to Prolog.

N. Ikeda, M.S., Computer Science, 1988. Making a Medical Expert System.

O.L. Astrachan, M.S., Computer Science, 1989. METEOR: Model Elimination Theorem-Proving for Efficient Or-Parallelism.

D.W. Reed, Ph.D., Computer Science, 1992. A Case-analysis Approach to Disjunctive Logic Programming.

O.L. Astrachan, Ph.D., Computer Science, 1992. Investigations in Model Elimination Based Theorem Proving.

T.S. Gegg-Harrison, Ph.D., Computer Science, 1993. Exploiting Program Schemata in a Prolog Tutoring System.

J.T. Girard, M.S., Computer Science, 1996. Automating the Communications Engineering Process using Expert System Technology.