A machine program for theorem-proving

@article{dpll-cacm5,
   abstract = {The programming of a proof procedure is discussed in connection with trial runs and possible improvements.},
   apice = {DpllCacm5},
   author = {Martin Davis and George Logemann and Donald Loveland},
   doi = {10.1145/368273.368557},
   eissn = {1557-7317},
   issn = {0001-0782},
   journal = {Communications of the ACM},
   month = jul,
   number = 7,
   numpages = 4,
   openalex = {W2057361103},
   pages = {394--397},
   publisher = {ACM},
   title = {A machine program for theorem-proving},
   url = {https://dl.acm.org/doi/10.1145/368273.368557},
   volume = 5,
   year = 1962
}