Our language for this is given by the grammar
statement : bool_exp
bool_exp : bndd_exp
| "(" "¬" bool_exp ")" | "(" bool_exp b_operator bool_exp ")"
| "(" quantifier variable "." bool_exp ")"
| "(" quantifier variable "<" bound ":" bool_exp ")"
| "[" "¬" bool_exp "]" | "[" bool_exp b_operator bool_exp "]"
| "[" quantifier variable "." bool_exp "]"
| "(" quantifier variable "<" bound ":" bool_exp "]"
| "{" "¬" bool_exp "}" | "{" bool_exp b_operator bool_exp "}"
| "{" quantifier variable "." bool_exp "}"
| "{" quantifier variable "<" bound ":" bool_exp "}"
| comparison
bndd_exp : "(" "¬" bndd_exp ")" | "(" bndd_exp b_operator bndd_exp ")"
| "(" quantifier variable "<" bound ":" bndd_exp ")"
| "[" "¬" bndd_exp "]" | "[" bndd_exp b_operator bndd_exp "]"
| "(" quantifier variable "<" bound ":" bndd_exp "]"
| "{" "¬" bndd_exp "}" | "{" bndd_exp b_operator bndd_exp "}"
| "{" quantifier variable "<" bound ":" bndd_exp "}"
| comparison
comparison : "(" num_exp c_relation num_exp ")"
| "[" num_exp c_relation num_exp "]"
| "{" num_exp c_relation num_exp "}"
b_operator : "∧" | "∨" | "⊃"
quantifier : "∀" | "∃"
variable : letter | variable "!"
variable : "v" | "w" | "x" | "y" | "z"
c_relation : "=" | "<" | ">" | "≤" | "≥"
bound : const_exp | variable
num_exp : bound | num_exp "'"
| "(" num_exp a_operator num_exp ")"
| "[" num_exp a_operator num_exp "]"
| "{" num_exp a_operator num_exp "}"
const_exp : "0" | const_exp "'"
| "(" const_exp a_operator const_exp ")"
| "[" const_exp a_operator const_exp "]"
| "{" const_exp a_operator const_exp "}"
a_operator : "+" | "-" | "·"