Syntax of logical formulas in Eos 3.3.2 (Revized 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 .