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.

✓ 3 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Context-Free Grammars and Normal Forms: Examples and Counterexamples

1 · Prerequisites

2 · Summary

These examples delete both nongenerating and unreachable symbols from a small grammar, realize the four basic CFL closure constructions on explicit languages, and show that an ambiguous grammar can still generate a language with an unambiguous presentation.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-30Open item page →

Removing one nongenerating variable and one unreachable variable

Example

Consider the grammar

S \to A B ∣ a, A \to a, B \to b, C \to c C, D \to d .

The variable $C$ is nongenerating, and $D$ is generating but unreachable from $S$ . Deleting both yields the smaller grammar

S \to A B ∣ a, A \to a, B \to b,

which generates the same language ${a b, a}$ .

Facts & Assumptions

Given: The grammar displayed above.

[L1]

Eliminating useless symbols preserves the generated language, by Eliminating useless symbols preserves the generated language.

Verification

technique · direct

1.1

The variable $C$ is nongenerating because its only production is $C \to c C$ , which never removes the variable $C$ . The variable $D$ is reachable from no sentential form derived from $S$ , because no production from $S$ , $A$ , or $B$ mentions $D$ .

given

2.1

Every terminal derivation from $S$ therefore uses only the variables $S$ , $A$ , and $B$ , and those derivations yield either $a$ or $a b$ . So deleting $C$ and $D$ leaves the language unchanged.

step 1.1

3.1

This is exactly the useless-symbol elimination guaranteed by [L1].

L1step 2.1∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-30Open item page →

One family of grammars realizing union, concatenation, star, and homomorphism

Example

Let $L_{1} = {a^{n} b^{n} : n \geq 0}, L_{2} = {c^{n} d^{n} : n \geq 0} .$ Standard grammars for them are $S_{1} \to a S_{1} b ∣ ε, S_{2} \to c S_{2} d ∣ ε .$

Then:

$L_{1} \cup L_{2}$ is generated by $S \to S_{1} ∣ S_{2}$ ,
$L_{1} L_{2}$ is generated by $S \to S_{1} S_{2}$ ,
$L_{1}^{*}$ is generated by $S \to ε ∣ S_{1} S$ ,
if $h (a) = 0$ and $h (b) = 1$ , then $\hat{h} (L_{1}) = {0^{n} 1^{n} : n \geq 0}$ .

Facts & Assumptions

Given: The two grammars for $L_{1}$ and $L_{2}$ , and the alphabet map with $h (a) = 0$ and $h (b) = 1$ .

[L1]

Context-free languages are closed under union, concatenation, Kleene star, and homomorphism, by Context-free languages are closed under union, concatenation, Kleene star, and homomorphism.

Verification

technique · direct

1.1

The bridge rules $S \to S_{1} ∣ S_{2}$ and $S \to S_{1} S_{2}$ give the listed grammars for the union and concatenation constructions, and the rule $S \to ε ∣ S_{1} S$ lists any finite concatenation of words from $L_{1}$ .

given

1.2

Replacing each terminal $a$ by $0$ and each terminal $b$ by $1$ turns the grammar for $L_{1}$ into one for ${0^{n} 1^{n} : n \geq 0}$ , which is exactly $\hat{h} (L_{1})$ .

given

2.1

These concrete constructions realize all four closure operations asserted in [L1].

L1step 1.1step 1.2∎

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-30Open item page →

An ambiguous expression grammar with an unambiguous grammar for the same language

Statement refuted

The statement "an ambiguous CFG always generates an inherently ambiguous language" is false.

Facts & Assumptions

Given: The ambiguous expression grammar $E \to E + E ∣ E * E ∣ (E) ∣ a ∣ b,$ and the precedence grammar $E \to E + T ∣ T, T \to T * F ∣ F, F \to (E) ∣ a ∣ b .$

[A1]

The statement refuted is: every ambiguous CFG generates an inherently ambiguous language.

[L1]

A context-free language is inherently ambiguous exactly when every context-free grammar generating it is ambiguous, by Ambiguous grammars, unambiguous grammars, and inherently ambiguous languages.

Counterexample

technique · direct

1.1

The first grammar is ambiguous because the word $a + a * a$ has both the parse $a + (a * a)$ and the parse $(a + a) * a$ .

given

1.2

The second grammar generates the same terminal strings as the first. One inclusion follows by simultaneous induction on its $E$ -, $T$ -, and $F$ -derivations, since every displayed production can be simulated by the first grammar. For the reverse inclusion, scan a generated word at parenthesis depth zero: split at its rightmost top-level + if one exists, otherwise at its rightmost top-level * if one exists, and otherwise recognize the forced factor $a$ , $b$ , or $(E)$ . Induction on word length gives a derivation in the second grammar. The same decomposition is unique: the $E$ -rule forces the rightmost top-level +, the $T$ -rule forces the rightmost top-level *, and the outer symbols force the $F$ -rule. Hence the second grammar is unambiguous and, in particular, $a + a * a$ has only the parse $a + (a * a)$ .

giveninduction

2.1

By [L1], a language with an unambiguous grammar is not inherently ambiguous. Therefore the first grammar is a counterexample to [A1].

A1L1step 1.1step 1.2∎

Context-Free Grammars and Normal Forms: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Removing one nongenerating variable and one unreachable variable

Example

Facts & Assumptions

Verification

One family of grammars realizing union, concatenation, star, and homomorphism

Example

Facts & Assumptions

Verification

An ambiguous expression grammar with an unambiguous grammar for the same language

Statement refuted

Facts & Assumptions

Counterexample

Sources