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 |