Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Modal Fragments

Nick Bezhanishvili, Balder ten Cate, Arunavo Ganguly, Arne Meier

Abstract

We survey systematic approaches to basis-restricted fragments of propositional logic and modal logics, with an emphasis on how expressive power and computational complexity depend on the allowed operators. The propositional case is well-established and serves as a conceptual template: Post's lattice organizes fragments via Boolean clones and supports complexity classifications for standard reasoning tasks. For modal fragments, we then bring together two historically independent lines of investigation: a general framework where modal fragments are parameterized by a basis of "connectives" defined by arbitrary modal formulas (initially proposed and studied by logicians such as Kuznetsov and Ratsa in the 1970s), and the more tractable class of what we call simple modal fragments parameterized by Boolean functions plus selected modal operators, where Post-lattice methods enable systematic decidability and dichotomy results. Along the way, we collect and extend results on teachability and exact learnability from examples for both propositional fragments and simple modal fragments, and we conclude by identifying several open problems.

Modal Fragments

Abstract

We survey systematic approaches to basis-restricted fragments of propositional logic and modal logics, with an emphasis on how expressive power and computational complexity depend on the allowed operators. The propositional case is well-established and serves as a conceptual template: Post's lattice organizes fragments via Boolean clones and supports complexity classifications for standard reasoning tasks. For modal fragments, we then bring together two historically independent lines of investigation: a general framework where modal fragments are parameterized by a basis of "connectives" defined by arbitrary modal formulas (initially proposed and studied by logicians such as Kuznetsov and Ratsa in the 1970s), and the more tractable class of what we call simple modal fragments parameterized by Boolean functions plus selected modal operators, where Post-lattice methods enable systematic decidability and dichotomy results. Along the way, we collect and extend results on teachability and exact learnability from examples for both propositional fragments and simple modal fragments, and we conclude by identifying several open problems.
Paper Structure (31 sections, 42 theorems, 23 equations, 4 figures, 1 table)

This paper contains 31 sections, 42 theorems, 23 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. Outline
  3. Preliminaries
  4. Relevant complexity classes
  5. Clones
  6. Boolean Clones
  7. Fragments of Classical Propositional Logic
  8. Expressive power and succinctness
  9. Complexity of expressibility and minimization
  10. Complexity of logical reasoning tasks
  11. Teachability and Learnability
  12. Fragments of Modal Logics
  13. Modal Fragments
  14. Modal Fragments via Modal Clones
  15. Simple Modal Fragments via Boolean Clones
  16. ...and 16 more sections

Key Result

Theorem 3.5

Let $O$ and $O'$ be finite sets of Boolean functions such that $\textup{\rm PL}_O$ and $\textup{\rm PL}_{O'}$ are expressively complete. Then there are polynomial-time truth-preserving translations between $\textup{\rm PL}_O$ and $\textup{\rm PL}_{O'}$, even in terms of tree-size.

Figures (4)

  • Figure 1: Post's Lattice
  • Figure 2: List of Abbreviations
  • Figure 3: The frame $G=(\mathbb{N}\cup\{\omega\},{>}\cup\{(\omega,\omega)\})$
  • Figure 4: Complexity of TBox satisfiability with respect to the logic $\mathbf{K}_\omega$ for simple multi-modal fragments $\textup{\rm ML}^\omega_{M\cup O}$, where $M\subseteq\{\Diamond_i,\Box_i\mid i\in\mathbb{N}\}$ and $O$ consists of purely propositional formulas. Also see Gen_Sat_ALC.

Theorems & Definitions (56)

  • Definition 2.1: Clones
  • Example 2.4
  • Remark 2.5
  • Example 3.1
  • Theorem 3.5: Pratt1975
  • Theorem 3.6: Thomas2012:applicability
  • Theorem 3.7: BohlerSchnoor2007
  • Theorem 3.8: Hemaspaandra2011:minimization
  • Theorem 3.9: Lewis_Sat_Problems_for_propositional_calculi
  • Theorem 3.10: Reith
  • ...and 46 more