A Machine Program for Theorem-Proving

Davis, M., Logemann, G., & Loveland, D. (1962). A Machine Program for Theorem-Proving. Communications of the ACM, 394-397.

Type

Journal article

Intellectual base

Primary research

Year

1962

DOI

10.1145/368273.368557

Link

https://doi.org/10.1145/368273.368557

Cited by

1 citation across 1 artifact.

Domain-specific

• Davis–Putnam Algorithm
  • DPLL replaces the potentially explosive exhaustive-resolution elimination step with case splitting and backtracking, while retaining unit propagation and related simplifications.

Verification

This reference passed the adversarial substantiation pipeline: it was checked to exist and to support the claim it is attached to. See how references were verified.

Registry ID ref:6d713dddf221 · see in the full table