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 |