Modal clausal form

Short description: A normal form for modal logic formulae

Modal clausal form, also known as separated normal form by modal levels (SNF_ml) and Mints normal form, is a normal form for modal logic formulae.

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.

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). Each modal level consists of three forms as follows.

• Literal clause: a disjunction of propositional literals [math]\displaystyle{ \bigvee_{b=1}^r l_b }[/math].
• Positive a-clause: [math]\displaystyle{ l' \to \Box_a l }[/math] where [math]\displaystyle{ l' }[/math] and [math]\displaystyle{ l }[/math] are propositional literals.
• Negative a-clause: [math]\displaystyle{ l' \to \Diamond_a l }[/math] where [math]\displaystyle{ l' }[/math] and [math]\displaystyle{ l }[/math] are propositional literals.

These three forms are also called cpl-clauses, box-clauses and dia-clauses respectively. Note that any clause in conjunctive normal form (CNF) is also a literal clause in this normal form.