Donald W. Loveland
According to our database^{1}, Donald W. Loveland
Awards
ACM Fellow
ACM Fellow 2000, "Played a major role in the development of theory proving and automated deduction through seminal research and an influential book on the subject.".
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:

at id.loc.gov

at dnb.info
On csauthors.net:
Bibliography
2016
Mark Stickel: His Earliest Work.
J. Autom. Reasoning, 2016
2003
Satchmorebid: Satchmo(Re) with BIDirectional Relevancy.
New Generation Comput., 2003
2000
Automated deduction: achievements and future directions.
Commun. ACM, 2000
1999
Automated Deduction: Looking Ahead.
AI Magazine, 1999
1997
The Use of Lemmas in the Model Elimination Procedure.
J. Autom. Reasoning, 1997
1995
SATCHMORE: SATCHMO with REIevancy.
J. Autom. Reasoning, 1995
NearHorn Prolog and the Ancestry Family of Procedures.
Ann. Math. Artif. Intell., 1995
Uniform Proofs and Disjunctive Logic Programming (Extended Abstract)
Proceedings of the Proceedings, 1995
1994
Proof Procedures for Disjunctive Logic Programming.
Proceedings of the Innovationen bei Rechen und Kommunikationssystemen, Eine Herausforderung für die Informatik, 24. GIJahrestagung im Rahmen des 13th World Computer Congress, IFIP Congress '94, Hamburg, 28. August, 1994
1992
A Comparison of Three Prolog Extensions.
J. Log. Program., 1992
On the complexity of belief network synthesis and refinement.
Int. J. Approx. Reasoning, 1992
1991
NearHorn Prolog and Beyond.
J. Autom. Reasoning, 1991
An Alternative Characterization of Disjunctive Logic Programs.
Proceedings of the Logic Programming, Proceedings of the 1991 International Symposium, San Diego, California, USA, Oct. 28, 1991
The NearHorn Approach to Disjunctive Logic Programming.
Proceedings of the Extensions of Logic Programming, Second International Workshop, 1991
A NearHorn Prolog for Compilation.
Proceedings of the Computational Logic  Essays in Honor of Alan Robinson, 1991
METEORs: High Performance Theorem Provers Using Model Elimination.
Proceedings of the Automated Reasoning: Essays in Honor of Woody Bledsoe, 1991
1988
A Simple NearHorn Prolog Interpreter.
Proceedings of the Logic Programming, 1988
An nHProlog Implementation.
Proceedings of the 9th International Conference on Automated Deduction, 1988
1987
Finding TestandTreatment Procedures Using Parallel Computation.
J. Parallel Distrib. Comput., 1987
Finding Critical Sets.
J. Algorithms, 1987
NearHorn PROLOG.
Proceedings of the Logic Programming, 1987
1986
Finding TestandTreatment Procedures Using Parallel Computation.
Proceedings of the International Conference on Parallel Processing, 1986
1985
Performance Bounds for Binary Testing with Arbitrary Weights.
Acta Inf., 1985
1983
Detecting Ambiguity: An Example in Knowledge Evaluation.
Proceedings of the 8th International Joint Conference on Artificial Intelligence. Karlsruhe, 1983
1981
Deleting Repeated Goals in the Problem Reduction Format.
J. ACM, 1981
1980
Simplifying Interpreted Formulas.
Proceedings of the 5th Conference on Automated Deduction, 1980
1978
Presburger Arithmetic with Bounded Quantifier Alternation
Proceedings of the 10th Annual ACM Symposium on Theory of Computing, 1978
Automated theorem proving: a logical basis.
Fundamental studies in computer science 6, NorthHolland, ISBN: 0720404991, 1978
1976
A Hole in Goal Trees: Some Guidance from Resolution Theory.
IEEE Trans. Computers, 1976
1974
An Implementation of the Model Elimination Proof Procedure.
J. ACM, 1974
1973
A Hole in Goal Trees: Some Guidance from Resolution Theory.
Proceedings of the 3rd International Joint Conference on Artificial Intelligence. Standford, 1973
1972
A Unifying View of Some Linear Herbrand Procedures.
J. ACM, 1972
1969
A Variant of the Kolmogorov Concept of Complexity
Information and Control, December, 1969
Erratum: "Mechanical TheoremProving by Model Elimination".
J. ACM, 1969
A Simplified Format for the Model Elimination TheoremProving Procedure.
J. ACM, 1969
On MinimalProgram Complexity Measures
Proceedings of the 1st Annual ACM Symposium on Theory of Computing, 1969
1968
Mechanical TheoremProving by Model Elimination.
J. ACM, 1968
1962
A machine program for theoremproving.
Commun. ACM, 1962