Such a normal form is commonly used for automated theorem proving using tableau calculi and resolution calculi techniques due to its benefits of better space bounds and improved decision procedures.
In normal modal logic, any set of formulae can be transformed into an equisatisfiable set of formulae in this normal form.
[3] In multimodal logic where a represents an agent corresponding to an accessibility relation function in Kripke semantics, a formula in this normal form is a conjunction of clauses labelled by the modal level (i.e., the number of nested modalities).
These three forms are also called cpl-clauses, box-clauses and dia-clauses respectively.
[4] Note that any clause in conjunctive normal form (CNF) is also a literal clause in this normal form.