Donald W. Loveland

J. Autom. Reason., 2016

DPLL: The Core of Modern Satisfiability Solvers.

[BibT_eX]

[DOI]

Ashish Sabharwal

Bart Selman

Proceedings of the Martin Davis on Computability, 2016

2003

Satchmorebid: Satchmo(Re) with BIDirectional Relevancy.

[BibT_eX]

[DOI]

Adnan H. Yahya

New Gener. Comput., 2003

2000

Automated deduction: achievements and future directions.

[BibT_eX]

[DOI]

Commun. ACM, 2000

1999

Automated Deduction: Looking Ahead.

[BibT_eX]

[DOI]

AI Mag., 1999

1997

The Use of Lemmas in the Model Elimination Procedure.

[BibT_eX]

[DOI]

Owen L. Astrachan

J. Autom. Reason., 1997

1995

SATCHMORE: SATCHMO with REIevancy.

[BibT_eX]

[DOI]

Debra Sue Wilson

J. Autom. Reason., 1995

Near-Horn Prolog and the Ancestry Family of Procedures.

[BibT_eX]

[DOI]

Ann. Math. Artif. Intell., 1995

Uniform Proofs and Disjunctive Logic Programming (Extended Abstract)

[BibT_eX]

[DOI]

Gopalan Nadathur

Proceedings of the Proceedings, 1995

1994

Proof Procedures for Disjunctive Logic Programming.

[BibT_eX]

[DOI]

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.

[BibT_eX]

[DOI]

J. Log. Program., 1992

On the complexity of belief network synthesis and refinement.

[BibT_eX]

[DOI]

Marco Valtorta

Int. J. Approx. Reason., 1992

1991

Near-Horn Prolog and Beyond.

[BibT_eX]

[DOI]

J. Autom. Reason., 1991

An Alternative Characterization of Disjunctive Logic Programs.

[BibT_eX]

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.

[BibT_eX]

[DOI]

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

A Near-Horn Prolog for Compilation.

[BibT_eX]

Proceedings of the Computational Logic - Essays in Honor of Alan Robinson, 1991

METEORs: High Performance Theorem Provers Using Model Elimination.

[BibT_eX]

Owen L. Astrachan

Proceedings of the Automated Reasoning: Essays in Honor of Woody Bledsoe, 1991

1988

A Simple Near-Horn Prolog Interpreter.

[BibT_eX]

Proceedings of the Logic Programming, 1988

An nH-Prolog Implementation.

[BibT_eX]

[DOI]

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

1987

Finding Test-and-Treatment Procedures Using Parallel Computation.

[BibT_eX]

[DOI]

J. Parallel Distributed Comput., 1987

Finding Critical Sets.

[BibT_eX]

[DOI]

J. Algorithms, 1987

Near-Horn PROLOG.

[BibT_eX]

Proceedings of the Logic Programming, 1987

1986

Automated theorem proving: mapping logic into AI.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGART International Symposium on Methodologies for Intelligent Systems, 1986

1985

Performance Bounds for Binary Testing with Arbitrary Weights.

[BibT_eX]

[DOI]

Acta Informatica, 1985

1983

Detecting Ambiguity: An Example in Knowledge Evaluation.

[BibT_eX]

[DOI]

Marco Valtorta

Proceedings of the 8th International Joint Conference on Artificial Intelligence. Karlsruhe, 1983

1981

Deleting Repeated Goals in the Problem Reduction Format.

[BibT_eX]

[DOI]

C. R. Reddy

J. ACM, 1981

1980

Simplifying Interpreted Formulas.

[BibT_eX]

[DOI]

Robert E. Shostak

Proceedings of the 5th Conference on Automated Deduction, 1980

1978

Presburger Arithmetic with Bounded Quantifier Alternation

[BibT_eX]

[DOI]

C. R. Reddy

Proceedings of the 10th Annual ACM Symposium on Theory of Computing, 1978

Automated theorem proving: a logical basis.

[BibT_eX]

[DOI]

Fundamental studies in computer science 6, North-Holland, ISBN: 0720404991, 1978

1976

A Hole in Goal Trees: Some Guidance from Resolution Theory.

[BibT_eX]

[DOI]

Mark E. Stickel

IEEE Trans. Computers, 1976

1974

Position statement: mathematical computer science courses.

[BibT_eX]

[DOI]

ACM SIGCSE Bull., 1974

The heart of computer science.

[BibT_eX]

[DOI]

Norman E. Gibbs

James M. Ortega

ACM SIGCSE Bull., 1974

An Implementation of the Model Elimination Proof Procedure.

[BibT_eX]

[DOI]

J. ACM, 1974

1972

A Unifying View of Some Linear Herbrand Procedures.

[BibT_eX]

[DOI]

J. ACM, 1972

1969

A Variant of the Kolmogorov Concept of Complexity

[BibT_eX]

[DOI]

Inf. Control., December, 1969

Erratum: "Mechanical Theorem-Proving by Model Elimination".

[BibT_eX]

[DOI]

J. ACM, 1969

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

[BibT_eX]

[DOI]

J. ACM, 1969

On Minimal-Program Complexity Measures

[BibT_eX]

[DOI]

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

1968

Mechanical Theorem-Proving by Model Elimination.

[BibT_eX]

[DOI]

J. ACM, 1968

1962

A machine program for theorem-proving.

[BibT_eX]

[DOI]

Martin Davis

George Logemann

Commun. ACM, 1962

1960

Empirical explorations of the geometry theorem machine.

[BibT_eX]

[DOI]

Herbert L. Gelernter

J. R. Hansen