Empirical explorations of the geometry theorem machine. - Herbert L. Gelernter; J. R. Hansen; Donald W. Loveland (IRE-AIEE-ACM Computer Conference (Western), 1960)

A machine program for theorem-proving. - Martin Davis; George Logemann; Donald W. Loveland (Commun. ACM, 1962)

Mechanical Theorem-Proving by Model Elimination. - Donald W. Loveland (J. ACM, 1968)

On Minimal-Program Complexity Measures - Donald W. Loveland (STOC, 1969)

A Simplified Format for the Model Elimination Theorem-Proving Procedure. - Donald W. Loveland (J. ACM, 1969)

Erratum: "Mechanical Theorem-Proving by Model Elimination". - Donald W. Loveland (J. ACM, 1969)

A Variant of the Kolmogorov Concept of Complexity - Donald W. Loveland (Inf. Control., 1969)

A Unifying View of Some Linear Herbrand Procedures. - Donald W. Loveland (J. ACM, 1972)

An Implementation of the Model Elimination Proof Procedure. - S. Fleisig; Donald W. Loveland; A. K. Smiley III; D. L. Yarmush (J. ACM, 1974)

The heart of computer science. - Norman E. Gibbs; Donald W. Loveland; James M. Ortega (ACM SIGCSE Bull., 1974)

Position statement: mathematical computer science courses. - Donald W. Loveland (ACM SIGCSE Bull., 1974)

A Hole in Goal Trees: Some Guidance from Resolution Theory. - Donald W. Loveland; Mark E. Stickel (IEEE Trans. Computers, 1976)

Automated theorem proving: a logical basis. - Donald W. Loveland (North-Holland, 1978)

Presburger Arithmetic with Bounded Quantifier Alternation - C. R. Reddy; Donald W. Loveland (STOC, 1978)

Simplifying Interpreted Formulas. - Donald W. Loveland; Robert E. Shostak (CADE, 1980)

Deleting Repeated Goals in the Problem Reduction Format. - Donald W. Loveland; C. R. Reddy (J. ACM, 1981)

Detecting Ambiguity: An Example in Knowledge Evaluation. - Donald W. Loveland; Marco Valtorta (IJCAI, 1983)

Performance Bounds for Binary Testing with Arbitrary Weights. - Donald W. Loveland (Acta Informatica, 1985)

Automated theorem proving: mapping logic into AI. - Donald W. Loveland (ISMIS, 1986)

Near-Horn PROLOG. - Donald W. Loveland (ICLP, 1987)

Finding Critical Sets. - Donald W. Loveland (J. Algorithms, 1987)

Finding Test-and-Treatment Procedures Using Parallel Computation. - Louis D. Duval; Robert A. Wagner; Yijie Han; Donald W. Loveland (J. Parallel Distributed Comput., 1987)

An nH-Prolog Implementation. - Bruce T. Smith; Donald W. Loveland (CADE, 1988)

A Simple Near-Horn Prolog Interpreter. - Bruce T. Smith; Donald W. Loveland (ICLP/SLP, 1988)

METEORs: High Performance Theorem Provers Using Model Elimination. - Owen L. Astrachan; Donald W. Loveland (Automated Reasoning: Essays in Honor of Woody Bledsoe, 1991)

A Near-Horn Prolog for Compilation. - Donald W. Loveland; David W. Reed (Computational Logic - Essays in Honor of Alan Robinson, 1991)

The Near-Horn Approach to Disjunctive Logic Programming. - David W. Reed; Donald W. Loveland; Bruce T. Smith (ELP, 1991)

An Alternative Characterization of Disjunctive Logic Programs. - David W. Reed; Donald W. Loveland; Bruce T. Smith (ISLP, 1991)

Near-Horn Prolog and Beyond. - Donald W. Loveland (J. Autom. Reason., 1991)

On the complexity of belief network synthesis and refinement. - Marco Valtorta; Donald W. Loveland (Int. J. Approx. Reason., 1992)

A Comparison of Three Prolog Extensions. - David W. Reed; Donald W. Loveland (J. Log. Program., 1992)

Proof Procedures for Disjunctive Logic Programming. - Donald W. Loveland (GI Jahrestagung, 1994)

Uniform Proofs and Disjunctive Logic Programming (Extended Abstract) - Gopalan Nadathur; Donald W. Loveland (LICS, 1995)

Near-Horn Prolog and the Ancestry Family of Procedures. - David W. Reed; Donald W. Loveland (Ann. Math. Artif. Intell., 1995)

SATCHMORE: SATCHMO with REIevancy. - Donald W. Loveland; David W. Reed; Debra Sue Wilson (J. Autom. Reason., 1995)

The Use of Lemmas in the Model Elimination Procedure. - Owen L. Astrachan; Donald W. Loveland (J. Autom. Reason., 1997)

Automated Deduction: Looking Ahead. - Donald W. Loveland (AI Mag., 1999)

Automated deduction: achievements and future directions. - Donald W. Loveland (Commun. ACM, 2000)

Satchmorebid: Satchmo(Re) with BIDirectional Relevancy. - Donald W. Loveland; Adnan H. Yahya (New Gener. Comput., 2003)

DPLL: The Core of Modern Satisfiability Solvers. - Donald W. Loveland; Ashish Sabharwal; Bart Selman (Martin Davis on Computability, Computational Logic, and Mathematical Foundations, 2016)

Mark Stickel: His Earliest Work. - Donald W. Loveland (J. Autom. Reason., 2016)