 In many recent publications on epistemic logic, the full set of formulas in the language is given using a so-called Backus-Naur Form (BNF). This is simply a notational technique derived from computer science that provides a recursive definition of the formulas deemed grammatically “correct”, i.e., the set of well-formed formulas: