# 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 Other## Links

#### 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

Near-Horn 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. GI-Jahrestagung 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

Near-Horn 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 Near-Horn Approach to Disjunctive Logic Programming.

Proceedings of the Extensions of Logic Programming, Second International Workshop, 1991

A Near-Horn 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 Near-Horn Prolog Interpreter.

Proceedings of the Logic Programming, 1988

An nH-Prolog Implementation.

Proceedings of the 9th International Conference on Automated Deduction, 1988

1987

Finding Test-and-Treatment Procedures Using Parallel Computation.

J. Parallel Distrib. Comput., 1987

Finding Critical Sets.

J. Algorithms, 1987

Near-Horn PROLOG.

Proceedings of the Logic Programming, 1987

1986

Finding Test-and-Treatment 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, North-Holland, 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 Theorem-Proving by Model Elimination".

J. ACM, 1969

A Simplified Format for the Model Elimination Theorem-Proving Procedure.

J. ACM, 1969

On Minimal-Program Complexity Measures

Proceedings of the 1st Annual ACM Symposium on Theory of Computing, 1969

1968

Mechanical Theorem-Proving by Model Elimination.

J. ACM, 1968

1962

A machine program for theorem-proving.

Commun. ACM, 1962