@article{Davis:1960:CPQ:321033.321034,
    Address = {New York, NY, USA},
    Author = {Davis, Martin and Putnam, Hilary},
    File = {A Computing Procedure for Quantification Theory - Davis, Putnam (0) (0) - a - a - y.pdf},
    ISSN = {0004-5411},
    Journal = {J. ACM},
    Keywords = {classic},
    Month = {July},
    Number = {3},
    Pages = {201--215},
    Publisher = {ACM},
    Title = {A Computing Procedure for Quantification Theory},
    URL = {http://doi.acm.org/10.1145/321033.321034},
    Volume = {7},
    Year = {1960},
    acmid = {321034},
    bdsk-url-1 = {http://doi.acm.org/10.1145/321033.321034},
    bdsk-url-2 = {http://dx.doi.org/10.1145/321033.321034},
    date-added = {2015-09-16 14:27:07 +0000},
    date-modified = {2015-09-16 14:27:10 +0000},
    issue_date = {July 1960},
    numpages = {15},
    doi = {10.1145/321033.321034}
}

@article{Davis:1960:CPQ:321033.321034, Address = {New York, NY, USA}, Author = {Davis, Martin and Putnam, Hilary}, File = {A Computing Procedure for Quantification Theory - Davis, Putnam (0) (0) - a - a - y.pdf}, ISSN = {0004-5411}, Journal = {J. ACM}, Keywords = {classic}, Month = {July}, Number = {3}, Pages = {201--215}, Publisher = {ACM}, Title = {A Computing Procedure for Quantification Theory}, URL = {http://doi.acm.org/10.1145/321033.321034}, Volume = {7}, Year = {1960}, acmid = {321034}, bdsk-url-1 = {http://doi.acm.org/10.1145/321033.321034}, bdsk-url-2 = {http://dx.doi.org/10.1145/321033.321034}, date-added = {2015-09-16 14:27:07 +0000}, date-modified = {2015-09-16 14:27:10 +0000}, issue_date = {July 1960}, numpages = {15}, doi = {10.1145/321033.321034} }