According to Wikipedia, Donald W. Loveland is a professor emeritus of computer science at Duke University who specializes in artificial intelligence. He is well known for the Davis–Putnam–Logemann–Loveland algorithm.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.

- A machine program for theorem-proving
- Automated theorem proving: a logical basis
- Mechanical Theorem-Proving by Model Elimination
- A Simplified Format for the Model Elimination Theorem-Proving Procedure
- A Linear Format for Resolution
- A Variant of the Kolmogorov Concept of Complexity
- Automated Theorem Proving: After 25 Years
- Presburger arithmetic with bounded quantifier alternation
- A New Interpretation of the von Mises' Concept of Random Sequence†
- Automated theorem proving: A logical basis (Fundamental studies in computer science)
- Empirical explorations of the geometry-theorem proving machine
- Near-Horn PROLOG
- Logical Foundations for Cognitive Agents: Contributions in Honor of Ray Reiter
- An Implementation of the Model Elimination Proof Procedure
- A Unifying View of Some Linear Herbrand Procedures
- Empirical explorations of the geometry theorem machine
- A Comparison of Three Prolog Extensions
- A Hole in Goal Trees: Some Guidance from Resolution Theory
- The Kleene hierarchy classification of recursively random sequences
- On minimal-program complexity measures
- Performance bounds for binary testing with arbitrary weights
- SATCHMORE: SATCHMO with RElevancy
- A Near-Horn Prolog for Compilation
- METEORs: High Performance Theorem Provers Using Model Elimination
- Automated theorem proving: a quarter-century review
- A Machine Program for Theorem-Provingt
- Handbook of Logic in Artificial Intelligence and Logic Programming, Volume2, Deduction Methodologies
- An Alternative Characterization of Disjunctive Logic Programs
- The Graduate Course Advisor: A Multi-Phase Rule-Based Expert System
- 6th Conference on Automated Deduction
- Theorem-Provers Combining Model Elimination and Resolution
- A Simple Near-Horn Prolog Interpreter
- The Use of Lemmas in the Model Elimination Procedure
- Detecting Ambiguity: An Example in Knowledge Evaluation
- On the complexity of belief network synthesis and refinement
- Proof Procedures for Logic Programming
- Near-Horn Prolog and beyond
- Automated theorem proving: mapping logic into AI
- Automated deduction: achievements and future directions
- Automated Deduction: Looking Ahead
- Uniform proofs and disjunctive logic programming
- The Near-Horn Approach to Disjunctive Logic Programming
- Simplifying Interpreted Formulas
- Deleting Repeated Goals in the Problem Reduction Format
- Finding Critical Sets
- Proceedings of the 6th Conference on Automated Deduction
- Some linear herbrand proof procedures : an analysis
- Three Views of Logic: Mathematics, Philosophy, and Computer Science
- DPLL: The Core of Modern Satisfiability Solvers
- Arithmetic Circuit Complexity and Motion Planning
- Near-Horn Prolog and the ancestry family of procedures
- The heart of computer science
- Finding Test-and-Treatment Procedures Using Parallel Computation
- A Other Related Work
- Uniform Proofs and Disjunctive Logic Programming (Extended Abstract)
- Automated Reasoning for Theory Building in the Social Sciences
- SATCHMOREBID: SATCHMO(RE) with BIDirectional relevancy
- Review: Robert Kowalski, Logic for Problem Solving
- Erratum: “Mechanical theorem-proving by model elimination”
- An Alternative Characterization of Disjunctive Logic Programs an Alternative Characterization of Disjunctive Logic Programs
- REFINEMENTS OF RESOLUTION
- Part 1. Proof Theory
- Position statement: mathematical computer science courses
- THE ROLE OF LOGICAL SYSTEMS
- CHAPTER 4 – SUBSUMPTION
- Uniform Proofs and Disjunctive Logic Programming (Extended
- 6th Conference on Automated Deduction, New York, USA, June 7-9, 1982
- An nH-Prolog Implementation
- Dipaola Robert A.. Random sets in subrecursive hierarchies. Journal of the Association for Computing Machinery, vol. 16 (1969), pp. 621–630.
- A HoleinGoalTrees: SomeGuidance fromResolution Theory
- CHAPTER 2 – BASIC RESOLUTION
- Three Views of Logic
- A Near-horn Prolog for Compilation a Near-horn Prolog for Compilation
- Representation and Decision Mechanisms in Artificial Intelligence.
- Review: V. N. Agafonov, Complexity of Computing Pseudorandom Sequences
- Search Algorithms and Their Implementationi U \ L ) Fz ~ . 2 BC 01 k
- Search Algorithms and Their Implementation.
- Empirical Expiorations of the Geometry Theorem Machine
- CHAPTER 6 – RESOLUTION AND PROBLEM REDUCTION FORMAT
- RESOLUTION WITH EQUALITY
- Inference and Decision Mechanisms in Artificial Intelligence
- Mark Stickel: His Earliest Work
- Arithmetic Circuit Complexity and Motion Planning Arithmetic Circuit Complexity and Motion Planning
- Proof Procedures for Disjunctive Logic Programming
- Proof Procedures for Logic Programming Proof Procedures for Logic Programming Y 1 Building the Framework: the Resolution Procedure 1.1 the Resolution Procedure
- Inference and Decision Mechanisms in Artificial Intelligence : Final Report

This paper list is powered by the following services:

Donald W. Loveland is affiliated with the following schools:

This website uses cookies to enhance the user experience. Privacy Policy

Stay informed! Get the latest Academic Influence news, information, and rankings with our upcoming newsletter.