Misplaced Pages

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 ${\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. 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.

This formal methods-related article is a stub. You can help Misplaced Pages by expanding it.

• v
• t
• e

v t e Normal forms in logic
Propositional logic	Negation normal form Conjunctive normal form Disjunctive normal form Algebraic normal form (Zhegalkin polynomial) Blake canonical form Canonical normal form Horn clause
Predicate logic	Skolem normal form Herbrandization Prenex normal form
Other	Beta normal form Modal clausal form Normal form (natural deduction)

• Normal forms (logic)
• Modal logic
• Formal methods stubs