The Complexity of Theorem-Proving Procedures

• p. 1 Section 1, first paragraph

  distinct function and predicate symbols

• p. 1 Section 1, first paragraph

  only have about n/logn distinct function and predicate symbols

Judge's note: Page 1 image: the sentence before this one describes proposition symbols (atoms) written as a member of Σ followed by a binary number. The 'Thus' conclusion then names function and predicate symbols, which belong to the predicate calculus of Section 3. The bound is right; the wording names the wrong kind of symbol.

Second check: another model agreed

• p. 4 Proof of Theorem 2, first sentence

  By the corollary to theorem 1, each of the sets is P-reducible to {DNF tautologies}.

• p. 2 Corollary

  Each of the sets in definitions 1)–5) is P-reducible to {DNF tautologies}.

Judge's note: Pages 2 and 4: definitions 1)–5) are subgraph pairs, isomorphic graphpairs, Primes, DNF tautologies and D3. {tautologies} is listed in Theorem 2 but is not in that list. The reduction does follow directly from Theorem 1, by the same complement argument the Corollary uses, so the pointer is imprecise rather than mathematically wrong.

Second check: another model agreed

• p. 3 Formula E, proof of Theorem 1

  q0 is the initial state

• p. 3 Proposition symbols and formula E

  Qi t for 1 ≤ i ≤ r, 1 ≤ t ≤ T

• p. 3 state set

  the set of states is {q1,...,qr}

Only the authors can say what is right here.

Judge's note: Page 3 image confirms the state set {q1,...,qr} (footnote 4 discusses only q_s versus q_r), the range 1 ≤ i ≤ r, and E = Q^0_1 ∧ ... with 'q0 is the initial state'. The index 0 falls outside the declared range, so D does not constrain Q^0_1 as written. Either the state set or the initial-state symbol needs adjusting. The proof idea is unaffected.

Second check: another model agreed

• p. 3 Proof of Theorem 1, definition of G^t_{i,j}

  where qk is the state given by the transition function for M

• p. 3 Displayed formula for G^t_{i,j}

  ¬Qi t ∨¬Ss,t ∨¬P j s,t ∨Qk t+1

Only the authors can say what is right here.

Judge's note: Page 3 image confirms the clause and its wording. My own check: suppose M's transition relation allows two moves from (q_i, σ_j) with different next states q_a and q_b. Any one q_k fixed in G, together with D (exactly one state per time), forces Q^k_{t+1} and so rules out the other branch. A(w) could then be unsatisfiable even though some branch accepts, so the 'iff' would fail. The text introduces G with 'For example', and footnote 5 notes an undeciphered handwritten annotation right here. The standard repair (a disjunction over the allowed moves, tied to F and H) keeps Theorem 1. The step is faulty; the stated result stands.

Second check: another model agreed

• p. 1 Heading of Section 1

  Tautologies and Polynomial Re-Reducibility.

• p. 1 Section 1 heading

  Polynomial Re-Reducibility

Judge's note: Page 1 image confirms the heading. The term 're-reducibility' is never defined or used anywhere else. It looks like a duplicated syllable, possibly carried over from the typescript.

Second check: none (judge only)

• p. 1 Footnote *

  I transcripted basically exactly

• p. 1 Footnote *

  I transcripted basically exactly as Cook wrote

Judge's note: Page 1 image: footnote * shows 'transcripted'. This is a non-standard word form in the transliterator's own note.

Second check: none (judge only)

• p. 2 Definition 3

  The set {Primes} is the set of all binary notations

• p. 3 Remark after Theorem 2

  add either {primes} or {isomorphic graphpairs}

• p. 3 Remark after Theorem 2

  We have not been able to add either {primes}

• p. 3 Remark

  add either {primes} or

Judge's note: The images on pages 2 and 3 confirm the different capitalisation and typeface for the same set. This is cosmetic only.

Second check: none (judge only)

• p. 3 Definition of C_{s,t}, proof of Theorem 1

  q ≤ t ≤ Tj

• p. 3 Definition of C in proof of Theorem 1

  For 1 ≤ s ≤ T and q ≤ t ≤ Tj Cs,t

• p. 3 definition of C

  For 1 ≤s ≤T and q ≤t ≤Tj Cs,t asserts

• p. 3 definition of C

  q ≤t ≤Tj Cs,t

Judge's note: Page 3 image shows 'q ≤ t ≤ T_j'. No T_j is defined, and q denotes states elsewhere. Every other time range in the construction is 1 ≤ t ≤ T. This is a typing slip.

Second check: none (judge only)

• p. 3 Paragraph after Remark

  Incidently, it is

• p. 3 after Remark

  Incidently

• p. 4 Discussion

  intractible

• p. 4 Discussion

  preceeding

Judge's note: Page 3 image confirms 'Incidently'. Footnote 6 corrects only the missing 'is'. The other two misspellings this cluster lists ('intractible', 'preceeding') are judged separately under C009 and C010.

Second check: none (judge only)

• p. 4 Section 2 Discussion, first paragraph

  apparently intractible

Judge's note: Page 4 image confirms the spelling 'intractible'.

Second check: none (judge only)

• p. 4 Section 2 Discussion, last paragraph

  the preceeding sections

Judge's note: Page 4 image confirms the spelling 'preceeding'.

Second check: none (judge only)

• p. 4 Proof of Theorem 2, D3 to subgraph reduction

  for each i, φ(i) = ui j for some j

• p. 4 Proof of Theorem 2, D3 to subgraph reduction

  such that for each i, φ(i) = ui j for some j

Judge's note: Page 4 image confirms 'φ(i) = u_ij' in two places. Identifying v_i with i is a common shorthand and the meaning is clear, but the paper never states it.

Second check: none (judge only)

• p. 4 Discussion

  normal disjunctive form

Judge's note: Page 4 image confirms the phrase. Elsewhere (pp. 2 and 4) the paper says 'disjunctive normal form'. This is a minor terminology inconsistency and the meaning is clear.

Second check: none (judge only)

• p. 6 proof of 3B

  since we can assume |A| ≤logk

Judge's note: Page images p5 and p6 checked. The definition on p5 has log with subscript 2. The proof of 3B on p6 has plain 'log k', and 3A also uses plain log ('m ≤ log s^2'). This is a notational inconsistency only. Plain log most likely means base 2 here, and a change of base is a constant factor that cannot affect the O(k log^2 k) bound, so the argument is unaffected. Cosmetic.

Second check: none (judge only)

• p. 7 Reference [7]

  Dominoes and the AEA case of the decision problems.

Only the authors can say what is right here.

Judge's note: Rests on outside knowledge: that Wang's 1962 paper is titled 'Dominoes and the AEA case of the decision problem' (singular). The p7 image confirms the plural 'problems' is printed. Nothing in the files can confirm the true title, so this is an author query. At most it is a one-letter slip in the title, and the citation can still be identified.

Second check: none (judge only)

• p. 7 References [5]

  J. Assoc. Computing Machinery, 1960, pp. 201–215.

Judge's note: The p7 reference list image confirms that [5] has only the year and pages, while [4], in the same journal, gives volume and number. This is a stylistic inconsistency in the bibliography, and the entry can still be identified from authors, year and pages. Supplying the volume and issue would rely on outside knowledge.

Second check: none (judge only)