DOI: 10.1145/368273.368557. A machine program for theorem-proving

10.1145/368273.368557

Crossref journal-article

Association for Computing Machinery (ACM)

Communications of the ACM (320)

Abstract

The programming of a proof procedure is discussed in connection with trial runs and possible improvements.

Bibliography

Davis, M., Logemann, G., & Loveland, D. (1962). A machine program for theorem-proving. Communications of the ACM, 5(7), 394â397.

Authors 3

Martin Davis (first)
George Logemann (additional)
Donald Loveland (additional)

References 3 Referenced 1,794

10.1145/321033.321034
10.1147/rd.41.0028
{'key': 'e_1_2_1_3_2', 'first-page': '2', 'article-title': 'An improved proof procedure', 'volume': '26', 'author': 'PRAWITZ DAG', 'year': '1960', 'journal-title': 'Theoria'} / Theoria / An improved proof procedure by PRAWITZ DAG (1960)

Dates

Type	When
Created	23 years, 1 month ago (July 27, 2002, 7:37 a.m.)
Deposited	2 months, 1 week ago (June 18, 2025, 6:54 p.m.)
Indexed	9 hours, 2 minutes ago (Aug. 29, 2025, 6:24 a.m.)
Issued	63 years, 1 month ago (July 1, 1962)
Published	63 years, 1 month ago (July 1, 1962)
Published Online	63 years, 1 month ago (July 1, 1962)
Published Print	63 years, 1 month ago (July 1, 1962)

Funders 0

None

BibTeX

@article{Davis_1962, title={A machine program for theorem-proving}, volume={5}, ISSN={1557-7317}, url={http://dx.doi.org/10.1145/368273.368557}, DOI={10.1145/368273.368557}, number={7}, journal={Communications of the ACM}, publisher={Association for Computing Machinery (ACM)}, author={Davis, Martin and Logemann, George and Loveland, Donald}, year={1962}, month=jul, pages={394–397} }

JSON

{
  "indexed": {
    "date-parts": [
      [
        2025,
        8,
        29
      ]
    ],
    "date-time": "2025-08-29T10:24:39Z",
    "timestamp": 1756463079883,
    "version": "3.41.0"
  },
  "reference-count": 3,
  "publisher": "Association for Computing Machinery (ACM)",
  "issue": "7",
  "license": [
    {
      "start": {
        "date-parts": [
          [
            1962,
            7,
            1
          ]
        ],
        "date-time": "1962-07-01T00:00:00Z",
        "timestamp": -236822400000
      },
      "content-version": "vor",
      "delay-in-days": 0,
      "URL": "https://www.acm.org/publications/policies/copyright_policy#Background"
    }
  ],
  "content-domain": {
    "domain": [
      "dl.acm.org"
    ],
    "crossmark-restriction": true
  },
  "published-print": {
    "date-parts": [
      [
        1962,
        7
      ]
    ]
  },
  "abstract": "<jats:p>The programming of a proof procedure is discussed in connection with trial runs and possible improvements.</jats:p>",
  "DOI": "10.1145/368273.368557",
  "type": "journal-article",
  "created": {
    "date-parts": [
      [
        2002,
        7,
        27
      ]
    ],
    "date-time": "2002-07-27T11:37:46Z",
    "timestamp": 1027769866000
  },
  "page": "394-397",
  "update-policy": "https://doi.org/10.1145/crossmark-policy",
  "source": "Crossref",
  "is-referenced-by-count": 1794,
  "title": "A machine program for theorem-proving",
  "prefix": "10.1145",
  "volume": "5",
  "author": [
    {
      "given": "Martin",
      "family": "Davis",
      "sequence": "first",
      "affiliation": [
        {
          "name": "Institute of Mathematical Sciences, New York Univ., New York"
        }
      ]
    },
    {
      "given": "George",
      "family": "Logemann",
      "sequence": "additional",
      "affiliation": [
        {
          "name": "Institute of Mathematical Sciences, New York Univ., New York"
        }
      ]
    },
    {
      "given": "Donald",
      "family": "Loveland",
      "sequence": "additional",
      "affiliation": [
        {
          "name": "Institute of Mathematical Sciences, New York Univ., New York"
        }
      ]
    }
  ],
  "member": "320",
  "published-online": {
    "date-parts": [
      [
        1962,
        7
      ]
    ]
  },
  "reference": [
    {
      "key": "e_1_2_1_1_2",
      "doi-asserted-by": "publisher",
      "DOI": "10.1145/321033.321034"
    },
    {
      "key": "e_1_2_1_2_2",
      "doi-asserted-by": "publisher",
      "DOI": "10.1147/rd.41.0028"
    },
    {
      "key": "e_1_2_1_3_2",
      "first-page": "2",
      "article-title": "An improved proof procedure",
      "volume": "26",
      "author": "PRAWITZ DAG",
      "year": "1960",
      "journal-title": "Theoria"
    }
  ],
  "container-title": "Communications of the ACM",
  "original-title": [],
  "language": "en",
  "link": [
    {
      "URL": "https://dl.acm.org/doi/10.1145/368273.368557",
      "content-type": "unspecified",
      "content-version": "vor",
      "intended-application": "text-mining"
    },
    {
      "URL": "https://dl.acm.org/doi/pdf/10.1145/368273.368557",
      "content-type": "unspecified",
      "content-version": "vor",
      "intended-application": "similarity-checking"
    }
  ],
  "deposited": {
    "date-parts": [
      [
        2025,
        6,
        18
      ]
    ],
    "date-time": "2025-06-18T22:54:03Z",
    "timestamp": 1750287243000
  },
  "score": 1,
  "resource": {
    "primary": {
      "URL": "https://dl.acm.org/doi/10.1145/368273.368557"
    }
  },
  "subtitle": [],
  "short-title": [],
  "issued": {
    "date-parts": [
      [
        1962,
        7
      ]
    ]
  },
  "references-count": 3,
  "journal-issue": {
    "issue": "7",
    "published-print": {
      "date-parts": [
        [
          1962,
          7
        ]
      ]
    }
  },
  "alternative-id": [
    "10.1145/368273.368557"
  ],
  "URL": "http://dx.doi.org/10.1145/368273.368557",
  "relation": {},
  "ISSN": [
    "0001-0782",
    "1557-7317"
  ],
  "subject": [],
  "container-title-short": "Commun. ACM",
  "published": {
    "date-parts": [
      [
        1962,
        7
      ]
    ]
  },
  "assertion": [
    {
      "value": "1962-07-01",
      "order": 2,
      "name": "published",
      "label": "Published",
      "group": {
        "name": "publication_history",
        "label": "Publication History"
      }
    }
  ]
}