Modal clausal form

Modal clausal form, also known as separated normal form by modal levels (SNF_ml)^[1] and Mints normal form,^[2] 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.^[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). Each modal level consists of three forms as follows.

• Literal clause: a disjunction of propositional literals ${\displaystyle \bigvee _{b=1}^{r}l_{b}}$.
• Positive a-clause: ${\displaystyle l'\to \Box _{a}l}$ where ${\displaystyle l'}$ and ${\displaystyle l}$ are propositional literals.
• Negative a-clause: ${\displaystyle l'\to \Diamond _{a}l}$ where ${\displaystyle l'}$ and ${\displaystyle l}$ are propositional literals.

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.

References

1. Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare (8 November 2015). A Modal-Layered Resolution Calculus for K. TABLEAUX 2015: Automated Reasoning with Analytic Tableaux and Related Methods, Wrocław, Poland. Lecture Notes in Computer Science. Vol. 9323. Cham: Springer. pp. 185–200. doi:10.1007/978-3-319-24312-2_13. ISBN 978-3-319-24312-2.
2. Mints, Grigori (1990). Gentzen-type systems and resolution rules part I propositional logic. COLOG 1988: International Conference on Computer Logic. Lecture Notes in Computer Science. Vol. 417. Berlin, Heidelberg: Springer. doi:10.1007/3-540-52335-9_55. ISBN 978-3-540-46963-6.
3. Goré, Rajeev; Nguyen, Linh Anh (12 August 2009). "Clausal Tableaux for Multimodal Logics of Belief". Fundamenta Informaticae. 94 (1). Polish Mathematical Society, IOS Press: 21–40. doi:10.3233/FI-2009-115.
4. Goré, Rajeev; Kikkert, Cormac (6 September 2021). CEGAR-Tableaux: Improved Modal Satisfiability via Modal Clause-Learning and SAT. TABLEAUX 2021: Automated Reasoning with Analytic Tableaux and Related Methods, Birmingham, UK. Lecture Notes in Computer Science. Vol. 12842. Cham: Springer. pp. 74–91. doi:10.1007/978-3-030-86059-2_5. ISBN 978-3-030-86059-2.