Class and Int language syntax can be described in the following BNF form:

Article → | "environ" Environment "text" Text |

Environment | → | Empty |

| | Proposition | |

| | Proposition ";" Environment |

Proposition | → | Formula |

| | Label ":" Formula |

Text | → | Empty |

| | Text-Item | |

| | Text-Item ";" Text |

Text-Item | → | Diffuse-Statement |

| | Compact-Statement |

Diffuse-Statement | → | "begin" Reasoning "end" |

| | Label ":" "begin" Reasoning "end" |

Compact-Statement | → | Proposition Justification |

Justification | → | Simple-Justification |

| | Proof |

Simple-Justification | → | Straightforward-Justification |

| | Auto-Justification |

Straightforward-Justification | → | Empty |

| | "by" Label-List |

Auto-Justification | → | "from" Label-List |

Proof | → | "proof" Reasoning "qed" |

Label-List | → | Label |

| | Label "," Label-List |

Reasoning | → | Empty |

| | Reasoning-Item | |

| | Reasoning-Item ";" Reasoning |

Reasoning-Item | → | Text-Item |

| | Assumption | |

| | Conclusion | |

| | Choice-Statement | |

| | Generalization | |

| | Examplification | |

| | Constant-Definition | |

| | Iterative-Equality |

Assumption | → | Single-Assumption |

| | Existential-Assumption |

Single-Assumption | → | "assume" Proposition |

Existential-Assumption | → | "given" Variable-List |

| | "given" Variable-List "such" "that" Proposition |

Conclusion | → | "thus" Text-Item |

Choice-Statement | → | "consider" Variable-List |

| | "consider" Variable-List "such" "that" Proposition Simple-Justification |

Generalization | → | "let" Variable-List |

| | "let" Variable-List "such" "that" Proposition |

Examplification | → | "take" Examples |

Examples | → | Example |

| | Example "," Examples |

Example | → | Term |

| | Equating |

Constant-Definition | → | "set" Equating-List |

Equating-List | → | Equating |

| | Equating "," Equating-List |

Equating | → | Variable "=" Term |

Iterative-Equality | → | Term "=" Term Simple-Justification Iterative-List |

Iterative-List | → | Iterative-Item |

| | Iterative-Item Iterative-List |

Iterative-Item | → | ".=" Term Simple-Justification |

Term | → | Variable |

| | Functor-Identifier "(" Arguments ")" |

Arguments | → | Empty |

| | Term-List |

Term-List | → | Term |

| | Term "," Term-List |

Formula | → | "for" Variable-List "holds" Formula |

| | "for" Variable-List "st" Formula "holds" Formula | |

| | "ex" Variable-List "st" Formula | |

| | Equivalence |

Equivalence | → | Implication |

| | Equivalence "iff" Implication |

Implication | → | Disjunction |

| | Implication "implies" Disjunction |

Disjunction | → | Conjunction |

| | Disjunction "or" Conjunction |

Conjunction | → | Multiplier |

| | Conjunction "&" Multiplier |

Multiplier | → | "not" Multiplier |

| | "(" Formula ")" | |

| | "true" | |

| | "false" | |

| | "contradiction" | |

| | "thesis" | |

| | Atom |

Atom | → | Predicate-Identifier "[" Arguments "]" |

| | Term "=" Term |

Variable-List | → | Variable |

| | Variable "," Variable-List |

Label | → | Numeral |

Variable | → | Identifier |

Functor-Identifier | → | Identifier |

Predicate-Identifier | → | Identifier |