알고리즘서지만 확인
A Computing Procedure for Quantification TheoryMartin Davis, Hilary Putnam · 1960Journal of the ACM 7(3), 201–215쪽 (1960)1차 술어 논리의 증명 절차를 컴퓨터에서 돌리는 방법을 다룬 논문으로, 명제 논리 부분을 처리하는 Davis–Putnam 절차의 출전으로 인용된다. 초록은 당시의 증명 프로그램들이 명제 계산 단계에서 막혔다는 문제의식에서 출발한다. 충족 가능성 판정 알고리즘의 역사를 Cook 의 정리(1971)보다 앞에서부터 적으려는 글에 필요하다. 이어진 구현은 dll-1962.
확인:Crossref 의 DOI 등록 기록으로 제목·저자·권호·쪽을 확인하고 같은 기록의 초록을 읽었다.