TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-09-12

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The CYK algorithm decides membership for CNF grammars

Statement

Let $G = (V, Σ, P, S)$ be a grammar in Chomsky normal form.

On input $ε$ , accept exactly when $S \to ε$ is a production of $G$ .
On input a nonempty word $w = a_{1} \dots a_{n}$ , fill the CYK table of $G$ on $w$ and accept exactly when $S \in T [1, n]$ .

This procedure decides whether $w \in L (G)$ .

Facts & Assumptions

Given: A CNF grammar $G = (V, Σ, P, S)$ and an input word $w$ .

[L1]

By A variable lies in a CYK table cell exactly when it derives that span, for a nonempty input word, $A \in T [i, ℓ]$ exactly when $A$ derives the corresponding span.

[L2]

By The language generated by a CFG, a word lies in $L (G)$ exactly when it is derivable from the start symbol $S$ .

Proof

technique · direct

1.1

If $w = ε$ , then by the definition of Chomsky normal form the only way to derive $ε$ is the exceptional start production $S \to ε$ . So the empty-word branch is correct.

L2given

1.2

Suppose $w = a_{1} \dots a_{n}$ is nonempty. By [L1], the condition $S \in T [1, n]$ is equivalent to $S \Rightarrow_{G}^{*} w$ . By [L2], that is equivalent to $w \in L (G)$ . Therefore the table branch accepts exactly the generated nonempty words.

L1L2given

2.1

The two branches together decide membership in $L (G)$ .

step 1.1step 1.2∎

Depends on

Used by

Context-free-language membership is decidable Corollary
FALSE: CYK needs no normal-form preprocessing False statement

Dependency tree · two levels

4 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Alfred V. Aho, COMS W3261 CS Theory, Lecture 10 (standard reference, not scraped)