Syntax of logical formulas in Eos 3.3.2 (Revised on 2021/4/2)
Syntax of logical formulas in Eos 3.3.2 (Revised on 2021/4/2)
◼
x** :: = a sequence of one or more symbols
◼
x* :: = null sequence | x**
◼
xs :: = x**
◼
simple-typedecl :: = x** | Element[ x, t]
◼
typedecl :: = simple-typedecl**
◼
formula :: = qff | Q[typedecl, formula]
◼
Q ::= Exists | ForAll
◼
qff ::= quantifier-free formula
This syntax of logical formulas defines the set of logical formulas used in Eos 3.3 .2 - .