On Modal Logic Formulae Minimization
                         Giovanni Pagliarini1 , Andrea Paradiso1 , Guido Sciavicco1 and Ionel Eduard Stan2
                         1
                             University of Ferrara, Italy
                         2
                             Free University of Bozen-Bolzano, Italy


                                         Abstract
                                         From the intricate circuits of digital devices to the abstract realms of logical theory, formula minimization remains
                                         a cornerstone challenge with various implications. This paper explores the adaptation of formula minimization
                                         techniques to modal logic 𝒦, driven by the challenges of processing increasingly complex data structures. Our
                                         investigation begins by analyzing the inherent computational complexity of minimizing modal formulae, a critical
                                         step towards developing effective solutions. We, then, introduce a heuristic algorithm for the purpose. We prove
                                         its correctness, addressing the unique demands of modal logic. The implications of this work extend beyond
                                         theoretical interest, and include practical insights for the post-hoc treatment of symbolic models in modal logic
                                         𝒦, as well as temporal, spatial, and other non-classical logics in advanced computational contexts.

                                         Keywords
                                         Modal logic, Formula minimization, Heuristic algorithm




                         1. Introduction
                         The expressiveness of two-valued Boolean algebra capable of describing switching circuit operations,
                         highlighted by Shannon in 1938 [1], allowed the arising of a new field called logic synthesis. The great
                         interest in circuits development, particularly in their Boolean form, highlighted a natural duality between
                         Boolean circuits and Boolean formulae; Boolean formulae can be considered a particular representation
                         of Boolean circuits. The need for ever smaller circuits and formula representations led to the study
                         of techniques whose goal was to reduce the dimension of a given circuit, preserving its semantic
                         behavior. To solve this problem, different algorithms were theorized, the most famous of which is the
                         Quine–McCluskey algorithm [2], considered a milestone in the field of logic optimization.
                            The challenge of reducing a Boolean circuit to its minimal equivalent can be adeptly transformed into
                         a logical problem using propositional logic. Specifically, given a Boolean formula 𝜙 and a metric for its
                         size (e.g., the number of tokens in the formula), the goal is to discover a formula 𝜙′ that is both equivalent
                         to 𝜙 and minimal in terms of size. This problem has been extensively examined when the formulae are
                         represented in disjunctive normal form (DNF) or conjunctive normal form (CNF), and we refer to it as the
                         Propositional Minimal Equivalent Formula (PMEF) problem, addressing it in both its search and decision
                         formats. The decision variant, in particular, is framed as follows: given a propositional formula 𝜙 and
                         an integer 𝑘, is there an equivalent formula 𝜓, whose size does not exceed 𝑘? Regardless of whether the
                         formula is presented in CNF, DNF, or another generic form, the complexity of PMEF is determined as
                         Σ𝑝2 -complete, as documented by [3]. This classification places it in the second level of the polynomial
                         hierarchy [4], distinct from the satisfiability problem (PSAT ), which well-knowingly Σ𝑝1 -complete, that
                         is, NP-complete.
                            Diverse strategies have been developed to address the PMEF problem, which can be categorized
                         into exact and heuristic algorithms. Exact methods inevitably grapple with the problem’s inherent
                         exponential time complexity yet consistently deliver globally minimal solutions. In contrast, heuristic
                         techniques strive to bypass the limitation of the required computational effort by offering solutions that
                         are good, though not necessarily optimal and represent local optima. Historically, exact algorithms

                          CILC 2024: 39th Italian Conference on Computational Logic, June 26-28, 2024, Rome, Italy
                          $ giovanni.pagliarini@unife.it (G. Pagliarini); andrea.paradiso@edu.unife.it (A. Paradiso); guido.sciavicco@unife.it
                          (G. Sciavicco); ioneleduardstan@unibz.it (I. E. Stan)
                           0000-0002-8403-3250 (G. Pagliarini); 0000-0002-3614-2487 (A. Paradiso); 0000-0002-9221-879X (G. Sciavicco);
                          0000-0001-9260-102X (I. E. Stan)
                                      © 2024 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).


CEUR
                  ceur-ws.org
Workshop      ISSN 1613-0073
Proceedings
have evolved from the foundational Quine-McCluskey algorithm. Notable implementations include
ESPRESSO [5], which operates in both exact and heuristic capacities, and SCHERZO [6], a state-of-
the-art solution. Prominent examples of heuristic algorithms are MINI [7], BOOM [8], and ESPRESSO,
again, which can function in both modalities. Moreover, recent advancements include a new algorithm
proposed in [9], which minimizes propositional formulae without translating into normal forms (CNF
or DNF).
   Beyond its foundational application in circuit minimization, propositional minimization finds rele-
vance in several domains. Notably, in the emerging field of eXplainable AI (XAI), this technique aids in
the post-hoc analysis of models, particularly in symbolic learning, where models are interpreted as sets
of propositional formulae. Such minimization processes are crucial, especially as outlined in [10], where
the role of prime implicants, a concept linked to formulae minimization, underscores their significance
in refining explanations within AI systems.
   While minimization has traditionally centered on propositional logic, similar inquiries can be ex-
tended to more expressive logical frameworks. For instance, first-order logic has been explored in this
context [11]. Our focus here is on modal logic, which augments propositional logic’s expressive power
without venturing into first-order complexities (refer to [12] for an overview). Modal logic is pivotal,
particularly as a foundational framework for more complex languages, including temporal [13, 14, 15],
spatial [16], and various description logics [17]. By examining the basic unary modal logic 𝒦, significant
insights can be gained, as evidenced by recent advances in symbolic learning beyond propositional
logic [18, 19, 20, 21], which are already apparent at this fundamental level [22]. Similarly to the proposi-
tional case, machine learned modal logic models—conceptualized as sets of modal formulae—can benefit
significantly from efficient minimization algorithms, especially since modal logic lacks a standardized
normal form, differentiating it markedly from propositional and first-order logics.
   In this work, we introduce the Modal Minimal Equivalent Formula (MMEF) problem, defined as the
search for the smallest modal formula equivalent to a given one. Its decision version asks whether a
modal formula 𝜓 exists, equivalent to 𝜙 and not exceeding a specified size 𝑘. We establish that MMEF
is PSPACE-complete, aligning its complexity with modal logic 𝒦 satisfiability testing (MSAT ). This
classification leads to a naïve but optimal exact algorithm that systematically explores all potential
smaller formulae within the original signature and verifies each for equivalence. The primary goal of
this paper is to propose an innovative heuristic algorithm for MMEF that leverages insights from its
propositional counterparts and to validate its correctness. As we will demonstrate, this heuristic is
uniquely adaptable and suitable for any extension of basic modal logic, regardless of the complexity or
variety of modal operators employed.
   This work is organized as follows. In Section 2 we briefly recall the basic modal logic, its syntax, and
its semantics. In Section 3 we define and study MMEF. Then, in Section 4 we describe our heuristic
solution, before concluding.


2. Modal Logic
The syntax of well-formed formulae in the basic modal language 𝒦 [12], denoted later by 𝜙, 𝜓, . . .
(the Greek letters 𝛼, 𝛽, . . ., instead, will be used to denote numeric parameters), is based on a set of
propositional letters 𝒫 = {𝑝, 𝑞, . . . }. Formulae are built with the following grammar:

                          𝜙 ::= ⊤ | ⊥ | 𝑝 | ¬𝜙 | 𝜙 ∧ 𝜙 | 𝜙 ∨ 𝜙 | ♢𝜙 | □𝜙,
where the missing classic Boolean operators can be obtained as shortcuts.
   The symbols ♢ and □ are called modalities, and, informally, they are treated as existential and
universal operator, respectively. A formula in which no modality occurs is said to be purely propositional,
or Boolean. Given two formulae 𝜙, 𝜓, we use 𝜙 = 𝜓 to denote the fact that they are syntactically
identical, and |𝜙| to denote the size of 𝜙. Several different, but substantially equivalent, size measures
of formula can be defined; the most common one is the number of tokens, that is, its length. In the
following, we shall assume that |𝜙| denotes precisely the length, but all our results immediately apply
to the other possibilites. The subset of 𝒫 that is used in a formula 𝜙, plus the symbols ⊤ and ⊥, is
called signature of 𝜙, and denoted by 𝑠𝑖𝑔(𝜙); given a signature 𝒮 ⊆ 𝒫 ∪ {⊤, ⊥}, we denote by Φ(𝒮)
the set of all well-formed modal formula that can be built on it. Finally, we denote by 𝑠𝑢𝑏(𝜙) the set of
all sub-formulae of a formula 𝜙; a formula 𝜓 ∈ 𝑠𝑢𝑏(𝜙) such that its outermost connective is a modal
operator, that is, a modal sub-formula, is said to be a maximally modal sub-formula if every sub-formula
𝜉 ∈ 𝑠𝑢𝑏(𝜙) such that 𝜓 ∈ 𝑠𝑢𝑏(𝜉) has, as outermost connective, a Boolean one, and the subset of 𝑠𝑢𝑏(𝜙)
of all and only maximally modal sub-formulae of a given formula 𝜙 is denoted by msub(𝜙).
   In the so-called Kripke semantics, we interpret a formula on a Kripke interpretation 𝐾 = (𝑊, 𝑅, 𝑉 ),
where the pair (𝑊, 𝑅), in which 𝑊 is a non-empty, finite set of worlds and 𝑅 ⊆ 𝑊 × 𝑊 is the
accessibility relation, is called Kripke frame, and 𝑉 is a valuation function that assigns to each world
the set of propositional letters that are true on it, that is 𝑉 : 𝑊 → 2𝒫 . In general, we denote Kripke
interpretations with the symbols 𝐾, 𝐾1 , . . .. Given an interpretation 𝐾 and a world 𝑤, we say that
𝐾, 𝑤 satisfies a formula 𝜙, denoted by 𝐾, 𝑤 |= 𝜙, if and only if

                     𝐾, 𝑤 |= 𝑝        iff   𝑝 ∈ 𝑉 (𝑤),
                     𝐾, 𝑤 |= ¬𝜙       iff   𝐾, 𝑤 ̸|= 𝜙,
                     𝐾, 𝑤 |= 𝜙 ∧ 𝜓    iff   𝐾, 𝑤 |= 𝜙 and 𝐾, 𝑤 |= 𝜓,
                     𝐾, 𝑤 |= 𝜙 ∨ 𝜓    iff   𝐾, 𝑤 |= 𝜙 or 𝐾, 𝑤 |= 𝜓,
                     𝐾, 𝑤 |= ♢𝜙       iff   ∃𝑣 s.t. 𝑤𝑅𝑣 and 𝐾, 𝑣 |= 𝜙,
                     𝐾, 𝑤 |= □𝜙       iff   ∀𝑣 s.t. 𝑤𝑅𝑣 it is the case that 𝐾, 𝑣 |= 𝜙.

Moreover, we have
                                                𝐾, 𝑤 |= ⊤,
                                                𝐾, 𝑤 ̸|= ⊥.
Given a modal formula 𝜙, we say that it is satisfiable if and only if there exists a Kripke interpretation
𝐾 and a world 𝑤 such that 𝐾, 𝑤 |= 𝜙; in this case, 𝐾 is said to be a model of 𝜙 (however, we often
use the term model to refer to machine learning models). In the following, we use the notation 𝜙 ≡ 𝜓
to denote the fact that 𝜙 and 𝜓 are equivalent, that is, for every interpretation 𝐾 and world 𝑤, it is
the case that 𝐾, 𝑤 |= 𝜙 if and only if 𝐾, 𝑤 |= 𝜓. Moreover, it is well-known that every modal logic
formula can be presented in negated normal form (NNF), that is, in such a way that the symbol ¬ only
occurs in front of propositional letters, and that converting a formula into an equivalent one in NNF
does not increase its length by more than a constant factor; in the following, we assume that every
formula is in NNF, and we use NNF() to denote an algorithm that turns a given formula in its negated
normal form equivalent. A propositional letters or the negation of a propositional letter is known as
a literal; here, we denote literals by 𝜆, 𝜆1 , . . .. Finally, given two formulae 𝜙, 𝜉, and given a formula
𝜓 ∈ 𝑠𝑢𝑏(𝜙), by 𝜙[𝜓/𝜉] we denote the formula 𝜙 after having syntactically replaced every occurrence
of the sub-formula 𝜓 in 𝜙 with 𝜉. Observe that modal logic generalizes propositional logic, and the
valuation function associates a propositional interpretation to each world. Later in this paper, we shall
use 𝑀, 𝑀1 , . . . to denote propositional interpretations.
   The satisfiability problem for modal logic (MSAT ), that is, the problem of establishing if, given a
modal formula, there exists a Kripke interpretation and a world that satisfy it, is known to be PSPACE-
complete [23]; this is in sharp contrast with the same problem at the propositional level (PSAT ), which is
NP-complete. There exist tens of available systems for satisfiability checking of modal formulae. These
are generally separated into tableau-based systems (e.g., [24, 25]), which can be considered extensions
of classical propositional tableaux, DPLL-based methods, that is, methods based on the progressive
substitution of modal sub-formulae with fresh propositional letters, so that standard propositional
satisfiability checkers can be then used (e.g., [26]), translational approaches, based on the idea of
translating a modal formula into its first-order counterpart, so that standard first-order satisfiability
checkers can be then used (e.g., [27]), and automata-based techniques (e.g., [28]); an excellent survey
on this topic can be found in [29]. In the following, we shall use PSAT() (resp., MSAT()) to denote an
algorithm that solves an instance of the satisfiability problem for propositional (resp., modal) logic.
   Modal logic is paradigmatic for several varieties of more-than-propositional logics. Indeed, most
classic temporal [13, 14, 15], spatial [16], and description [17] logics are specializations of modal logics
with more than one accessibility relations (possibly with higher arities) and associated modalities,
subject to constraints on the admitted Kripke interpretations, that range from very simple and intuitive
ones (e.g., transitivity, antisymmetry) to very complex ones (e.g., when worlds are assumed to be
intervals and modalities are assumed to mimic relations between intervals).


3. Exact Minimization of Modal Formulae
At the propositional level, the problem of minimizing a given formula has been presented in several
forms. In its decision version it is usually defined as the problem, given a formula 𝜙 and an integer 𝑘,
of establishing whether a formula 𝜓, smaller than or of the same size of 𝜙, and equivalent to 𝜙, exists.
Typically, propositional formulae are assumed to be in disjunctive normal form (DNF) or conjunctive
normal form (CNF), but the problem can be defined for generic formulae as well; as a matter of fact,
this problem is studied in [9]. Regardless of the form of the input formula, this problem, called here
the Propositional Minimal Equivalent Formula (PMEF) problem, is known to be Σ𝑝2 -complete [3]. In the
following, we shall use PMEF() to denote both an algorithm that solves an instance (𝜙, 𝑘) of the decision
version of this problem and an algorithm that solves an instance 𝜙 of its search counterpart. Whenever
convenient, we shall use EXACT-PMEF() (resp., HEURISTIC-PMEF()) to denote an exact (resp., heuristic)
algorithm for solving a particular instance.
  Generalizing the minimization problem to modal formulae is very natural. However, modal formulae
do not have an accepted disjunctive/conjunctive normal form in the same way that propositional ones
do; normal forms for modal formulae have been studied in [30], but the available proposals lack the
naturalness and simplicity that are characteristic of normal forms.

Definition 1. Given a modal formula 𝜙 and an integer 𝑘, the Modal Minimal Equivalent Formula
(MMEF) problem consists in deciding whether there exists a formula 𝜓 such that 𝜓 ≡ 𝜙 and its size is at
most 𝑘.

In the following, we shall use the same symbol to denote both the decision and the search version of this
problem. Similarly to the propositional case, in its search version this problem too can be solved exactly
and heuristically, and we shall use EXACT-MMEF() (resp., HEURISTIC-MMEF()) to denote a generic exact
(resp., heuristic) algorithm for it.

Lemma 1. MMEF is PSPACE-hard.

Proof: We aim to establish the PSPACE-hardness of MMEF through a Turing reduction from MSAT.
Consider an instance 𝜙 of MSAT. Notably, 𝜙 is unsatisfiable if and only if it is equivalent to the formula
⊥. Let us define 𝜓 = 𝜙 ∧ 𝑝 ∧ 𝑞, where 𝑝 and 𝑞 are propositional letters not included in 𝑠𝑖𝑔(𝜙), the
signature of 𝜙; we convert the instance 𝜙 for MSAT into the instance (𝜓, 1) for MMEF.
   Firstly, assume 𝜙 is satisfiable. Under this condition, any formula 𝜉 equivalent to 𝜙 and minimal
in size cannot be shorter than a single syntactic token (i.e., 𝜉 must be equivalent to ⊤ or to a single
propositional letter), and, in particular, cannot be 𝑝 nor 𝑞. Consequently, any minimal size formula 𝜁
equivalent to 𝜓 must, at least, include the conjunction 𝑝 ∧ 𝑞. Therefore, querying MMEF(𝜓, 1) under
these conditions would return false. Conversely, if 𝜙 is unsatisfiable, it is equivalent to ⊥, and so is 𝜓.
In this scenario, MMEF(𝜓, 1) would return true, indicating that a minimal formula equivalent to 𝜓 and
smaller than or equal to size 1 exists.
   This construction shows that MSAT ≤𝑇 MMEF. Given that MSAT is known to be PSPACE-hard, it
follows that MMEF is also PSPACE-hard.                                                                   □
As a side observation, it is easy to see that the above argument could be generalized to prove that the
minimization problem in any non-trivial logic is at least as hard as its satisfiability problem.
 Algorithm 1: Exact Modal Minimal Equivalent Formula
1   function EXACT-MMEF(𝜙):
2       forall 𝑘 ≤ |𝜙| do
 3          forall 𝜓 ∈ Φ(𝑠𝑖𝑔(𝜙)) of length 𝑘 do
 4               if EQUIVALENT (𝜙, 𝜓) then
  5                  return 𝜓
 6               end
 7          end
 8      end
 9      return 𝜙
10 end
11 function EQUIVALENT (𝜙, 𝜓):
12      return not MSAT ((𝜙 ∧ ¬𝜓) ∨ (𝜓 ∧ ¬𝜙))
13 end




   As it turns out, MMEF is also in PSPACE. This can be proved by providing a sound and complete
PSPACE algorithm for the search version of MMEF, that is, EXACT-MMEF(), shown in Alg. 1. Observe,
in particular, line 2 and 3 of EXACT-MMEF(): our systematic, ordered exploration of the search space
for 𝜓 ∈ Φ(𝑠𝑖𝑔(𝜙)) guarantees that this step does not require more than polynomial space, as it can be
implemented without memorizing smaller formulae.

Lemma 2. EXACT-MMEF() is terminating, sound and complete. Specifically, if 𝜓 = EXACT-MMEF(𝜙),
then:
     (i) 𝜓 ≡ 𝜙 and
    (ii) for every formula modal formula 𝜉, if |𝜉| < |𝜓|, then 𝜉 ̸≡ 𝜙.

Proof: It is immediate to observe that, for a given 𝜙, the execution EXACT-MMEF(𝜙) always termi-
nates.
   Suppose 𝜓 = EXACT-MMEF(𝜙). This implies that the query MSAT((𝜓 ∧ ¬𝜙) ∨ (𝜙 ∧ ¬𝜓)) returns
false, indicating that (𝜓 ∧ ¬𝜙) ∨ (𝜙 ∧ ¬𝜓) is unsatisfiable. Consequently, the equivalence 𝜓 ↔ 𝜙 holds,
verifying that 𝜓 ≡ 𝜙 and establishing (𝑖).
   For (𝑖𝑖), assume by contradiction that there exists a modal formula 𝜉 such that |𝜉| < |𝜓| and 𝜉 ≡ 𝜙.
Given that |𝜉| < |𝜓|, 𝜉 would have been tested for equivalence with 𝜙 before 𝜓. But since 𝜉 ≡ 𝜙, then
MSAT((𝜉 ∧ ¬𝜙) ∨ (𝜙 ∧ ¬𝜉)) would have returned false, so EXACT-MMEF(𝜙) would have returned 𝜉,
which is in contradiction with our assumption that EXACT-MMEF(𝜙) has returned 𝜓. Therefore no
such 𝜉 can exist, concluding the proof.                                                              □

Lemma 3. MMEF is in PSPACE.

Proof: Consider the operation of EXACT-MMEF(). The algorithm functions within polynomial space
bounds, as it tests each formula sequentially and discards each partial result; the space requirement for
each test is also polynomial. To solve a decision instance (𝜙, 𝑘) for MMEF, EXACT-MMEF() is executed
on 𝜙. Subsequently, the size of the resulting formula is compared to the integer 𝑘. Since EXACT-MMEF()
operates within polynomial space and the size comparison also requires only a constant amount of
additional space, MMEF is PSPACE.                                                                      □

Theorem 1. MMEF is PSPACE-complete.

  It is worth observing that our approach for EXACT-MMEF() is substantially equivalent to the naïve
approach for EXACT-PMEF() as shown in [9], used by the authors as baseline.
 Algorithm 2: Heuristic Modal Minimal Equivalent Formula
1   function HEURISTIC-MMEF(𝜙, 𝛼, 𝛽, 𝛾):
2       return HMMEF(𝜙, 𝛼, 𝛽, 𝛾, |𝜙|, 𝑠𝑖𝑔(𝜙))
 3 end
 4 function HMMEF(𝜙, 𝛼, 𝛽, 𝛾, Max , 𝒮):
  5     if |𝜙| ≤ 𝛼 then
  6          return EXACT-MMEF(𝜙)
  7     else
  8          if 𝜙 = 𝜙1 ⊚ 𝜙2 then
  9               (𝜓, 𝐻) ← PROPOREPLACE(𝜙, 𝛾, ∅, Max , 𝒮)
10                if |𝜓| ≤ 𝛽 then
 11                    𝜓 ′ ← EXACT-PMEF(𝜓, 𝛾)
12                else
 13                    𝜓 ′ ← HEURISTIC-PMEF(𝜓, 𝛾)
14                end
15                (𝜙, 𝐻) ← PROPOREPLACE(NNF (𝜓 ′ ), 𝛾, 𝐻 −1 , 0, 𝒮)
16           end
17           if 𝜙 = 𝜙1 ⊚ 𝜙2 then
18                return HMMEF(𝜙1 , 𝛼, 𝛽, 𝛾, Max , 𝒮) ⊚ HMMEF(𝜙2 , 𝛼, 𝛽, 𝛾, Max , 𝒮)
19           else if 𝜙 = ♢ 𝜙1 then
20                return ♢ HMMEF(𝜙1 , 𝛼, 𝛽, 𝛾, Max , 𝒮)
21           end
22      end
23 end




4. Heuristic Minimization of Modal Formulae
The naïve PSPACE approach to formula minimization, as discussed, exhibits considerable inefficiency.
This inefficiency stems primarily from three sources: unavoidable redundant exploration of formulae
equivalent to those already tested, inherently exponential time required for each test, and exponentially
wide search space. While the first issue could be partially mitigated by incorporating sorting techniques
to organize formulae, and the second one by employing very efficient implementations of MSAT solvers,
the number of potential candidates remains the most relevant bottleneck of this approach.
    To develop a more practical solution, we consider a heuristic approach that does not ensure a global
optimum but offers more operational feasibility. Drawing inspiration from [26], this approach exploits
efficient solutions to the PMEF problem. By progressively applying consistent substitutions, we aim
to minimize the initial formula at least from a propositional standpoint. It is important to note that
propositional minimization generally surpasses mere satisfiability checking in complexity, and most
current methods require the formula to be in a specific normal form. However, as demonstrated in [9],
it is feasible to minimize propositional formulae without converting them to normal form. Alternatively,
one could temporarily transform propositional sub-formulae into CNF or DNF for exact or heuristic
minimization, and subsequently assessing whether the resultant formula is indeed smaller than the
original. Throughout this process, we transition from exact to heuristic minimization methods based
on practical considerations. To ensure consistency in substitutions, an external hash table keyed by
the formulae themselves is utilized. This structure also aids in identifying semantically opposite sub-
formulae, a task that can be executed through exact or heuristic methods. For modal sub-formulae
that are sufficiently short, exact minimization remains feasible. In summary, our recursive, heuristic
approach hinges on three key parameters: 𝛼, the maximum length of a modal sub-formula below which
exact minimization is employed (as opposed to continuing recursion in search of smaller alternatives);
𝛽, the cutoff length for employing exact over heuristic minimization for propositional sub-formulae;
and 𝛾, the threshold under which exact substitutions are preferred to heuristic substitutions.
   HEURISTIC-MMEF(), outlined in Algorithm 2, serves as a simple driver for the recursive HMMEF()
function. The parameters 𝛼, 𝛽, and 𝛾 are natural numbers that modulate the optimizations within the
algorithm. Initially, HMMEF() checks if the input formula 𝜙 is small enough (|𝜙| ≤ 𝛼); if so, EXACT-
MMEF() is invoked directly. If |𝜙| exceeds 𝛼, HHMEF() evaluates the structure of 𝜙. For formulae where
the outermost connective is modal (i.e., 𝜙 = ♢ 𝜓 with ♢ ∈ {♢, □}), HHMEF() recursively calls itself
on its argument (i.e., 𝜓). If, on the other hand, the outermost connective is Boolean (i.e., 𝜙 = 𝜓1 ⊚ 𝜓2 ),
the process resorts to Boolean minimization.
   PROPOREPLACE() utilizes a hash table 𝐻, keyed by modal formulae, to manage substitutions. For
a given formula 𝜙 and any sub-formula 𝜓 ∈ 𝑠𝑢𝑏(𝜙), 𝐻[𝜓] stores the literal 𝜆 replacing 𝜓 in 𝜙 after
substitution. The goal of PROPOREPLACE() is to recursively substitute sub-formulae in 𝜙 with fresh
literals or their negations to render the formula purely propositional. Each execution begins with an
empty 𝐻. In the simplest case where 𝜙 is already a literal, no substitution is necessary. If the outermost
operator is modal and 𝜙 is sufficiently short (|𝜙| ≤ 𝛾), PROPOREPLACE() explores all smaller potential
equivalent formulae within 𝜙’s signature. If a formula 𝜓 is found to be semantically equivalent to 𝜙 (or
¬𝜙), PROPOREPLACE() checks if a literal 𝜆 has already been assigned to it and returns that literal (or its
negation). If no such 𝜓 is found (including the case where 𝜓 is 𝜙 itself), indicating that 𝜙 has not been
substituted previously, a fresh literal is assigned, updating 𝐻 with both 𝜙 and ¬𝜙. This substitution is
deemed exact. Conversely, if 𝜙 is too lengthy, PROPOREPLACE() repeats these steps but limits its scope
to checking if 𝐻 already contains 𝜙 or its negated form in NNF. If absent, a new fresh literal is assigned,
noting that this substitution may not be optimal as it might replace two equivalent sub-formulae with
different literals. When the outermost operator of 𝜙 is Boolean, PROPOREPLACE() recursively calls
itself on the inner sub-formulae, performs the replacements, and reconstructs the formula. Here, 𝐻
may remain unchanged but could be updated during the recursive calls.
  Because HEURISTIC-MMEF() is not an exact algorithm, we can only prove its soundness; to this
end, we first need to prove the soundness of PROPOREPLACE(). In the following, we assume that
HEURISTIC-MMEF() is called on some formula 𝜙 with 1 ≤ 𝛼, 𝛽, 𝛾 ≤ |𝜙|, that Max is the length of the
formula onto which HEURISTIC-MMEF() is called, and that 𝒮 its signature.

Lemma 4. If (𝜓, 𝐻) = PROPOREPLACE(𝜙, 𝛾, ∅, Max, 𝒮) and msub(𝜙) = {𝜓1 , . . . , 𝜓𝑛 }, then:
   (i) 𝜓 is Boolean,
  (ii) 𝜓 = 𝜙[𝜓1 /𝐻[𝜓1 ], . . . , 𝜓𝑛 /𝐻[𝜓𝑛 ]], and
 (iii) if 𝐻[𝜓𝑖 ] = 𝐻[𝜓𝑗 ] (resp., 𝐻[𝜓𝑖 ] = ¬𝐻[𝜓𝑗 ]) for some 𝑖 ̸= 𝑗, then 𝜓𝑖 ≡ 𝜓𝑗 (resp., 𝜓𝑖 ≡ ¬𝜓𝑗 ).

Proof: We proceed by double induction on the structural complexity of 𝜙 and the recursive depth of
the call to prove a stronger property. If (𝜓, 𝐻 ′ ) = PROPOREPLACE(𝜙, 𝛾, 𝐻, Max, 𝒮), then:
   (i) 𝜓 = 𝜙[𝜉1 /𝐻 ′ [𝜉1 ], . . . , 𝜉𝑛 /𝐻 ′ [𝜉𝑛 ]] for all maximal modal sub-formulae 𝜉1 , . . . , 𝜉𝑛 of 𝜙, unless 𝜙
       is a literal,
  (ii) if 𝜓 is a literal not in 𝒮, then 𝐻 ′ [𝜓] exists,
 (iii) for any pair of formulae 𝜉 ′ , 𝜉 ′′ , 𝐻 ′ [𝜉 ′ ] = 𝐻 ′ [𝜉 ′′ ] (resp., 𝐻 ′ [𝜉 ′ ] ≡ ¬𝐻 ′ [𝜉 ′′ ]) implies 𝜉 ′ ≡ 𝜉 ′′ (resp.,
       𝜉 ′ ≡ ¬𝜉 ′′ ), and
 (iv) for any formula 𝜉, 𝐻[𝜉] maps to a literal that is either ˜𝑡 or ¬𝑡˜, where ˜𝑡 ∈                / 𝒮.
   Assume that 𝜙 is a literal, that is, 𝜙 = 𝑝 or 𝜙 = ¬𝑝; by construction, it must be the case that 𝑝 ∈ 𝒮.
Then, PROPOREPLACE() returns (𝜓, 𝐻 ′ ) = (𝜙, 𝐻). If this is the first call to PROPOREPLACE(), then
both 𝐻 and 𝐻 ′ are empty, and if it is not, then 𝐻 remains unchanged from the previous call; in both
cases, (𝑖) – (𝑖𝑣) trivially hold. This solves the base case along both dimensions, that is, the call number
and the complexity of the input formula; all other cases are inductive.
   If the outermost connective of 𝜙 is a modal operator, we examine cases based on the size of 𝜙
relative to 𝛾. For 𝜙 with size less than or equal to 𝛾, all smaller NNF formulae within the signature
𝑠𝑖𝑔(𝜙) are considered. If a formula 𝜉 is such that 𝜉 ≡ 𝜙 (resp., 𝜉 ≡ ¬𝜙) exists with preassigned
𝐻[𝜉], we return (𝐻[𝜉], 𝐻) (resp., (𝐻[¬𝜉], 𝐻)). Then, (𝑖) and (𝑖𝑖) are satisfied trivially, and (𝑖𝑖𝑖)
and (𝑖𝑣) hold by inductive hypothesis. If no such 𝜉 is found, ˜𝑡 is introduced, and we return (𝑡˜, 𝐻 ′ )
setting 𝐻 ′ [𝜙/𝑡˜, NNF (¬𝜙)/¬𝑡˜]. Once more, (𝑖) and (𝑖𝑖) hold trivially; (𝑖𝑖𝑖) and (𝑖𝑣), instead, come by
 Algorithm 3: Propositional Replace
1   function PROPOREPLACE(𝜙, 𝛾, 𝐻, Max , 𝒮):
2       if 𝜙 = 𝑝 or 𝜙 = ¬𝑝 then
  3          if 𝑝 ∈ 𝒮 then
  4                 return (𝜙, 𝐻)
  5          else
  6                 return (𝐻[𝜙], 𝐻)
  7          end
  8     else if 𝜙 = ♢ 𝜙1 then
  9          if |𝜙| ≤ 𝛾 then
10                  forall 𝑘 ≤ Max do
 11                       forall 𝜓 ∈ Φ(𝑠𝑖𝑔(𝜙)) such that 𝜓 is in NNF and |𝜓| = 𝑘 do
 12                           if EQUIVALENT(𝜓, 𝜙) and 𝐻[𝜓] exists then
 13                                return (𝐻[𝜓], 𝐻)
 14                           end
 15                       end
16                  end
17                 ˜𝑡 ← NEWLETTER()
18                  𝐻[𝜙] ← ˜𝑡
19                  𝐻[NNF (¬𝜙)] ← ¬𝑡˜
20                  return (𝐻[𝜙], 𝐻)
21           else
22                  if 𝐻[𝜙] exists then
 23                       return (𝐻[𝜙], 𝐻)
24                  else
 25                      ˜𝑡 ← NEWLETTER()
 26                       𝐻[𝜙] ← ˜𝑡
 27                       𝐻[NNF (¬𝜙)] ← ¬𝑡˜
 28                       return (𝐻[𝜙], 𝐻)
29                  end
30           end
31      else if 𝜙 = 𝜙1 ⊚ 𝜙2 then
32           (𝜙′1 , 𝐻1 ) ← PROPOREPLACE (𝜙1 , 𝛾, 𝐻, Max , 𝒮)
33           (𝜙′2 , 𝐻2 ) ← PROPOREPLACE (𝜙2 , 𝛾, 𝐻1 , Max , 𝒮)
34           return (𝜙′1 ⊚ 𝜙′2 , 𝐻2 )
35      end
36 end




construction, because ˜𝑡 is fresh. If |𝜙| > 𝛾, then we proceed exactly in the same way, but limiting our
search to 𝜉 = 𝜙 and 𝜉 = NNF (¬𝜙), leading to exactly the same conclusions.
  Lastly, if 𝜙 = 𝜙1 ⊚ 𝜙2 , where ⊚ ∈ {∧, ∨}, recursive calls process sub-formulae 𝜙1 and 𝜙2 . After the
call on 𝜙1 and 𝐻, PROPOREPLACE() returns the pair (𝜙′1 , 𝐻1 ). After the second call, on 𝜙2 and 𝐻1 ,
PROPOREPLACE() returns the pair (𝜙′2 , 𝐻2 ). Then, the pair (𝜓, 𝐻 ′ ) = (𝜙′1 ⊚ 𝜙′2 , 𝐻2 ) is returned. At
this point, (𝑖) holds because msub(𝜙) = msub(𝜙′1 ) ∪ msub(𝜙′2 ), and (𝑖𝑖) holds trivially. Finally, (𝑖𝑖𝑖)
and (𝑖𝑣) hold by construction, and by the inductive hypothesis for 𝐻1 and 𝐻2 .                         □

Lemma 5. If it is the case that (𝜓, 𝐻) = PROPOREPLACE(𝜙, 𝛾, ∅, Max, 𝒮), 𝜓 ′ = PMEF(𝜓), and
(𝜓 ′′ , 𝐻) = PROPOREPLACE(𝜓 ′ , 𝛾, 𝐻 −1 , Max, 𝒮), then 𝜓 ′′ ≡ 𝜙.

Proof: We aim to demonstrate that for any Kripke interpretation 𝐾 = (𝑊, 𝑅, 𝑉 ) and world 𝑤, if
𝐾, 𝑤 |= 𝜙, then 𝐾, 𝑤 |= 𝜓 ′′ , and the other way around. Consider a Kripke interpretation 𝐾 and a
world 𝑤 such that 𝐾, 𝑤 |= 𝜙. Define 𝐾 ′ = (𝑊, 𝑅, 𝑉 ′ ) where 𝑉 ′ behaves as 𝑉 on every world and
every propositional letter 𝑝 ∈ 𝑠𝑖𝑔(𝜙), while, for a generic world 𝑤 and letter ˜𝑡 ∈
                                                                                  / 𝑠𝑖𝑔(𝜙) is defined as
follows:
                                                        and 𝐾, 𝑤 |= 𝜉, or
                                       {︂ −1
                      ˜𝑡 ∈ 𝑉 ′ (𝑤) iff   𝐻 [𝑡˜] = 𝜉
                                         𝐻 −1 [𝑡˜] = ¬𝜉 and 𝐾, 𝑤 ̸|= 𝜉
with 𝜉 ∈ msub(𝜙). Observe, first, that 𝐾 ′ is well-defined, thanks to Lemma 4, (𝑖𝑖𝑖). Moreover, since
 𝐾, 𝑤 |= 𝜙, by Lemma 4, (𝑖𝑖) and (𝑖𝑖𝑖), we know that 𝐾 ′ , 𝑤 |= 𝜓. Then, again by Lemma 4, (𝑖), we
 know that 𝜓 is a propositional formula, so that PMEF() can be applied to it; clearly, the resulting formula
 𝜓 ′ is equivalent to 𝜓, so that 𝐾 ′ , 𝑤 |= 𝜓 ′ . Now, we want to prove that 𝐾 ′ , 𝑤 |= 𝜓 ′′ , and we proceed by
 structural induction on 𝜓 ′ .
    If 𝜓 ′ = 𝑝 or 𝜓 ′ = ¬𝑝 for 𝑝 ∈ 𝒮, then 𝜓 ′′ = 𝜓 ′ and the claim follows directly. If 𝜓 ′ = ˜𝑡 (or ¬𝑡˜), where
   / 𝒮, then 𝜓 ′′ = 𝜉 for some 𝜉 ∈ msub(𝜙) such that 𝐻[𝜉] = ˜𝑡 (or 𝐻[𝜉] = ¬𝑡˜). Given that 𝐾 ′ , 𝑤 |= ˜𝑡
˜𝑡 ∈
 (or 𝐾 ′ , 𝑤 ̸|= ˜𝑡), by definition 𝐾 ′ , 𝑤 |= 𝜉 follows.
    Assume, now, 𝜓 ′ = 𝜁1′ ∧𝜁2′ . If 𝐾 ′ , 𝑤 |= 𝜓 ′ , then both 𝐾 ′ , 𝑤 |= 𝜁1′ and 𝐾 ′ , 𝑤 |= 𝜁2′ . Since 𝜓 ′′ = 𝜁1′′ ∧𝜁2′′
where 𝜁1′′ , 𝜁2′′ are the results from a call to PROPOREPLACE() on 𝜁1′ , 𝜁2′ , by the induction hypothesis
 𝐾 ′ , 𝑤 |= 𝜁1′′ and 𝐾 ′ , 𝑤 |= 𝜁2′′ , hence 𝐾 ′ , 𝑤 |= 𝜓 ′′ . The disjunction case 𝜓 ′ = 𝜁1′ ∨ 𝜁2′ is analogous.
    Finally, because 𝐾 ′ , 𝑤 |= 𝜓 ′′ and 𝑠𝑖𝑔(𝜓 ′′ ) = 𝑠𝑖𝑔(𝜙), it follows that 𝐾, 𝑤 |= 𝜓 ′′ as well, thereby
 concluding that 𝐾, 𝑤 |= 𝜙. The converse, that 𝐾, 𝑤 |= 𝜓 ′′ implies 𝐾, 𝑤 |= 𝜙, follows by a similar
 argument.                                                                                                             □
Lemma 6. If 𝜓 = HHMEF(𝜙, 𝛼, 𝛽, 𝛾, Max, 𝒮), then 𝜓 ≡ 𝜙 and |𝜓| ≤ |𝜙|.

Proof: We use induction on the complexity of 𝜙 to establish that if 𝜓 results from any invocation of
HHMEF(𝜙, 𝛼, 𝛽, 𝛾, Max, 𝒮), then 𝜓 ≡ 𝜙. Additionally, we aim to show that |𝜓| ≤ |𝜙|.
   Consider the case when |𝜙| ≤ 𝛼. In this scenario, 𝜓 is derived from the exact minimization of 𝜙.
Exact minimization ensures that 𝜓 is equivalent to 𝜙 and its size is less than or equal to that of 𝜙,
directly fulfilling the lemma’s conditions.
   Now, let us examine the situation where |𝜙| > 𝛼. If 𝜙 takes the form 𝜙1 ⊚ 𝜙2 , then after one
substitution with PROPOREPLACE(), one propositional minimization, and one back substitution, again,
with PROPOREPLACE(), we obtain 𝜓 ′ . Then Lemma 5 applies, and 𝜓 ′ ≡ 𝜙; thanks to the minimization
step, |𝜓 ′ | ≤ |𝜙|. At this point, three possibilities arise. If 𝜓 ′ is a literal, then 𝜓 = 𝜓 ′ , and the lemma
is satisfied. If 𝜓 ′ = 𝜓1′ ⊚ 𝜓2′ , then, in general, 𝜓 ′ may be different from 𝜙; yet, HMMEF() is called
recursively on 𝜓1′ and 𝜓2′ , returning 𝜓1 and 𝜓2 , respectively. By inductive hypothesis, 𝜓1 ≡ 𝜓1′ (resp.,
𝜓2 ≡ 𝜓2′ ) and |𝜓1 | ≤ |𝜓1′ (resp., |𝜓2 | ≤ |𝜓2′ ). But then, as we wanted, 𝜓 ≡ 𝜙 and |𝜓| ≤ |𝜙|. Finally,
if 𝜓 ′ = ♢ 𝜓1′ , then again, in general, 𝜓 ′ may be different from 𝜙; yet, HMMEF() is called recursively
on 𝜓1′ , returning 𝜓1 and, by inductive hypothesis, 𝜓1 ≡ 𝜓1′ and |𝜓1 | ≤ |𝜓1′ . Therefore, 𝜓 ≡ 𝜙 and
|𝜓| ≤ |𝜙|.                                                                                                    □
Theorem 2. HEURISTIC-MMEF() is sound, that is, if 𝜓 = HEURISTIC-MMEF(𝜙, 𝛼, 𝛽, 𝛾), then 𝜓 ≡ 𝜙
and |𝜓| ≤ |𝜙|.
  It is quite trivial to see that HEURISTIC-MMEF() works in polynomial space; however, it is worth dis-
cussing its temporal complexity. Let 𝒞HEURISTIC-MMEF (𝑛, 𝛼, 𝛽, 𝛾) denote the cost of executing HEURISTIC-
MMEF() on a formula of length 𝑛, with parameters 𝛼, 𝛽, and 𝛾, can be now estimated. A straight-
forward computation of its growth rate might not yield insightful results due to its heavy depen-
dence on several factors: the cost 𝒞EXACT-MMEF from each of the multiple runs of EXACT-MMEF(),
𝒞EXACT-PMEF from each of the various executions of EXACT-PMEF(), 𝒞HEURISTIC-PMEF from the calls to
HEURISTIC-PMEF(), and 𝒞PSAT from the applications of PSAT(). Nevertheless, it is possible to see that
𝒞HEURISTIC-MMEF (𝑛, 𝛼, 𝛽, 𝛾) = 𝒪(𝒞EXACT-MMEF (𝑛)), that is, that the heuristic approach is expected not to
perform worse than the exact method.
  We establish this by setting 𝛼 at some given fixed value, while 𝛽 and 𝛾 are configured to their worst-
case scenarios. Intuitively, as 𝛼 increases, HEURISTIC-MMEF()’s behavior more closely approximates
that of EXACT-MMEF(). When 𝛽 and 𝛾 are maximized, EXACT-PMEF() is utilized more frequently as
opposed to HEURISTIC-PMEF(), which inherently increases computational costs. Additionally, this
configuration leads to a higher frequency of PSAT() calls, further influencing the overall computational
expense.
Theorem 3. HEURISTIC-MMEF() is at least as efficient as EXACT-MMEF(), that is, 𝒞HEURISTIC-MMEF (𝑛, 𝛼,
𝛽, 𝛾) = 𝒪(𝒞EXACT-MMEF (𝑛)).
Proof: We start by noting that the worst case for HEURISTIC-MMEF() occurs when we set 𝛽 = 𝛾 = 𝑛.
Here, we analyze its computational complexity under these parameters, denoted as 𝒞HEURISTIC-MMEF (),
and show that it is bounded by 𝒪(𝒞EXACT-MMEF (𝑛)).
   Consider a modal formula of length 𝑛. In the most challenging scenario for HEURISTIC-MMEF(),
EXACT-MMEF() is invoked frequently on sub-formulae of length 𝛼. This scenario typically arises when
𝑛 symbols are distributed across the maximum number of sub-formulae, each comprising 𝛼 symbols; at
most, such sub-formulae can be 𝛼𝑛 . Each application of EXACT-MMEF() on these 𝛼-long sub-formulae
entails a cost of 𝒪(𝒞EXACT-MMEF (𝛼)). Moreover, again in the worst case, we can bound the cost due to the
remaining operations as follows. Each sub-formula goes through three steps: a call to PROPOREPLACE()
to perform a substitution, a call to EXACT-PMEF() (since 𝛽 = 𝑛), and a call to PROPOREPLACE()
to perform the back substitution. While the last operation only adds 𝒪(𝑛) to the total cost, the first
one consists of the entire exploration of the sub-formula (𝒪(𝑛)) plus an examination of each of 𝒪(2𝑛 )
potentially equivalent formulae (since 𝛾 = 𝑛) and a call to PSAT() (𝒞PSAT (𝑛)). Summing up the costs,
we derive:
                                          𝑛
        𝒞HEURISTIC-MMEF (𝑛, 𝛼, 𝛽, 𝛾) = 𝑂( 𝒞EXACT-MMEF (𝛼) + 𝑛(𝑛2𝑛 𝒞PSAT (𝑛) + 𝒞PMEF (𝑛) + 𝑛)).
                                          𝛼
Since 𝛼 is a constant, and since each call to EXACT-MMEF(𝜙), where |𝜙| = 𝑛, requires 𝒪(2𝑛 ) calls to
MSAT(), that is, it entails a cost of 𝒪(2𝑛 𝒞MSAT (𝑛)), we have that:

        𝒞HEURISTIC-MMEF (𝑛, 𝛼, 𝛽, 𝛾) = 𝑂 (𝑛(𝑛2𝑛 𝒞PSAT (𝑛) + 𝒞PMEF (𝑛) + 𝑛)) = 𝒪(2𝑛 𝒞MSAT (𝑛)),

the latter being precisely 𝒪(𝒞EXACT-MMEF (𝑛)), and hence we have the claim.                                □
  We conclude by showing an example of execution of HEURISTIC-MMEF() on the formula:

         𝜙 = (□(𝑝 → (𝑟 ∧ 𝑟))) ∧ ((𝑞 ∧ (𝑟 ∧ 𝑞))) ∧ (((□𝑞 ∧ ♢⊤) → ♢𝑞) ∧ □(𝑝 → (𝑟 ∧ 𝑟))),

shown in Fig. 1. Upon calling HEURISTIC-MMEF(𝜙, 8, 0, 0), after the first substitution step, we obtain a
propositional formulas as in Fig. 1a, middle, with a corresponding hash table as in Fig. 1a, right; observe
that, in the figure, we do not show the negations of formulae in 𝐻, which are nonetheless present.
Step 1 of the execution consists of substituting all maximally modal sub-formulae of 𝜙 with fresh
propositional letter; since |𝜙| = 28, no exact modal minimization is performed at this point. In Step 2,
shown in Fig. 1b, a heuristic propositional minimization is performed because 𝛽 = 0, which results
in the elimination of one redundant occurrence of ˜𝑡1 (in this case, however, an exact propositional
minimization would not have had a different result). Even after Step 3, that is, the reverse substitution of
the maximally modal formulae found in Step 1, shown in Fig. 1c, the hash table 𝐻 remains the same. At
this point, HEURISTIC-MMEF() is called, recursively, on the sub-formula rooted at ∧1 , with no changes,
on the sub-formula at □2 , which is minimized exactly, on the sub-formula rooted at ∧4 , with no result,
and on the sub-formula rooted at →5 , again, for an exact minimization; this process is shown in Fig. 1d.
   Observe that calling HEURISTIC-MMEF() on 𝜙 with a lower 𝛼 would lead to the result in Fig. 1d, left,
which is still smaller than the original one, but not as small as the result of the call with 𝛼 = 8.


5. Conclusions
Formula minimization is a well-known problem in the case of Boolean logic, with several applications
not only in field of circuit design but also in the area of explainable artificial intelligence. In this paper
we defined the same problem for the harder case of modal logic, motivated not only by the naturalness
of the question but also by the fact that modal logic is now being applied to learning from non-tabular
data, leading to the need of simplifying potentially very long modal formulas in order to ensure their
intepretability.
   We proved that the decision problem that corresponds to minimization in the modal case is PSPACE-
complete, and we proposed a heuristic algorithm, namely HEURISTIC-MMEF(), for it; we proved the
soundness of our proposal, and we discussed its theoretical complexity.
                                                                                                                                                                                        𝐻
                                     ∧
                                                                                                                              ∧                                                  key          value
           ∧                                                 ∧
                                                                                                      ∧                                                   ∧                 □(𝑝 → (𝑟 ∧ 𝑟))     𝑡˜1
     □                  ∧                              →                □              (1)
                                                                                       =⇒     𝑡˜1             ∧                                 →             𝑡˜1                □𝑞            𝑡˜2
     →              𝑞           ∧                ∧      ♢               →
                                                                                                          𝑞           ∧                     ∧           𝑡˜4                      ♢⊤            𝑡˜3
 𝑝       ∧                  𝑟        𝑞       □         ♢𝑞 𝑝                 ∧
                                                                                                                  𝑟           𝑞       𝑡˜2         𝑡˜3                            ♢𝑞            𝑡˜4
     𝑟          𝑟                            𝑞         ⊤                𝑟          𝑟

(a) In Step 1, since |𝜙| > 𝛼 a call to PROPREPLACE() is made and every maximally modal subformula, starting
    from the root, is substituted with a fresh propositional letter.
                                                                                                                                                                                        𝐻
                                         ∧                                                                                                                                       key          value
                                                                                                                                  ∧
                ∧                                                  ∧                                                                                                        □(𝑝 → (𝑟 ∧ 𝑟))     𝑡˜1
                                                                                       (2)            ∧                                                  →
         𝑡˜1                ∧                              →            𝑡˜1            =⇒                                                                                        □𝑞            𝑡˜2
                                                                                              𝑡˜1             ∧                                   ∧               𝑡˜4
                        𝑞            ∧                 ∧         𝑡˜4                                                                                                             ♢⊤            𝑡˜3
                                                                                                          𝑞               𝑟                 𝑡˜2         𝑡˜3
                                𝑟        𝑞       𝑡˜2       𝑡˜3                                                                                                                   ♢𝑞            𝑡˜4

(b) In Step 2, since |𝜙| > 𝛽, a call to HEURISTIC-PMEF() is made resulting in the elimination of 𝑡1 from the
    rightmost conjunct.
                                                                                                                                                                                        𝐻
                                                                                                                                  ∧
                                                                                                                                                                                  key         value
                                             ∧                                                        ∧                                                       →
                                                                                                                                                                            □(𝑝 → (𝑟 ∧ 𝑟))     𝑡˜1
                    ∧                                              →                   (3)        □               ∧                               ∧                     ♢
                                                                                       =⇒                                                                                         □𝑞            𝑡˜2
          𝑡˜1                   ∧                            ∧           𝑡˜4                      →           𝑞           𝑟                 □           ♢               𝑞
                        𝑞                                                                                                                                                         ♢⊤            𝑡˜3
                                     𝑟                 𝑡˜2        𝑡˜3                        𝑝        ∧                                     𝑞           ⊤
                                                                                                                                                                                  ♢𝑞            𝑡˜4
                                                                                                  𝑟       𝑟

                                             (c) In Step (3) a call to PROPREPLACE() operates the back substitution.
                                             ∧
                                                                                                                                      ∧
                    ∧1                                             →5                                                                                                                   𝐻∧4
                                                                                                                      ∧                                 ⊤
          □2                    ∧4                           ∧                 ♢         (4-11)                                                                                   key         value
                                                                                          =⇒                  □                   ∧
          →                 𝑞        𝑟                 □         ♢             𝑞                                                                                            □(𝑝 → (𝑟 ∧ 𝑟))     𝑡˜1
                                                                                                              →               𝑞         𝑟
     𝑝          ∧3                                     𝑞         ⊤
                                                                                                          𝑝           𝑟
           𝑟            𝑟

(d) From Step 4 to Step 11 several recursive calls are performed. In particular, from Step 4 to Step 7 the formula
    rooted at ∧1 is minimized, but no changes occur. Step (8) corresponds to a call to EXACT-MMEF() on the
    formula rooted at □2 (since its length is less than 𝛼), resulting into the elimination of the redundant conjunction
    𝑟 ∧ 𝑟. In Step 9 and 10 a recursive call on the formula rooted at ∧4 is performed, with no result. Finally, in
    Step (11) the procedure calls itself on the formula rooted at →5 ; since the length of this formula is less than 𝛼,
    again, this call corresponds to an execution of EXACT-MMEF(), leading to the final formula. The hash table
    shown at this point is precisely the one built within the recursive call on the formula rooted at ∧1 . Nodes in
    formula syntax trees are numbered following the recursive call at which they are considered; similarly, 𝐻4
    indicates the hash table at the fourth recursive call, that is, the last one in which a modification occurs.

Figure 1: Example of execution of HEURISTIC-MMEF().


  The natural continuation of this work is to implement HEURISTIC-MMEF() and to perform a com-
prehensive test to assess its practical usefulness. Moreover, as it is customary with heuristic solutions,
some different choices may lead to different behaviours in terms of practical efficiency; we plan to
explore several natural combinations and potential improvements of our proposals towards an optimal
solution. Finally, it would be interesting to establish to what extent the properties of specific modal
logics may improve the behaviour of HEURISTIC-MMEF() in specific cases, such as temporal or spatial
logics.
  This work is part of a long-term open-source project for symbolic learning and reasoning with modal,
temporal, and spatial logic, written in Julia language [31].


Acknowledgments
This research has been partially funded by the FIRD project Modal Geometric Symbolic Learning (Uni-
versity of Ferrara), and the Gruppo Nazionale Calcolo Scientifico-Istituto Nazionale di Alta Matematica
(GNCS-INdAM) project Symbolic and Numerical Analysis of Cyber-Physical Systems (GNCS-INdAM).
Giovanni Pagliarini, Guido Sciavicco, and Ionel Eduard Stan are GNCS-INdAM members.


References
 [1] C. E. Shannon, A symbolic analysis of relay and switching circuits, Transactions of the American
     Institute of Electrical Engineers (1938).
 [2] W. V. Quine, The problem of simplifying truth functions, The American Mathematical Monthly
     (1952).
 [3] C. Umans, The minimum equivalent dnf problem and shortest implicants, Journal of Computer
     and System Sciences (2001).
 [4] A. R. Meyer, L. J. Stockmeyer, The equivalence problem for regular expressions with squaring
     requires exponential space, in: Proc. of the 13th Annual Symposium on Switching and Automata
     Theory, 1972, pp. 125–129.
 [5] R. Rudell, A. Sangiovanni-Vincentelli, Multiple-valued minimization for pla optimization, IEEE
     Transactions on Computer-Aided Design of Integrated Circuits and Systems 6 (1987) 727–750.
 [6] O. Coudert, Doing two-level logic minimization 100 times faster, in: Proc. of the 6th Annual
     ACM-SIAM Symposium on Discrete Algorithms, 1995, pp. 112–121.
 [7] S. Hong, R. Cain, D. Ostapko, Mini: A heuristic approach for logic minimization, IBM Journal of
     Research and Development 18 (1974) 443 – 458.
 [8] J. Hlavicka, P. Fiser, BOOM - A heuristic boolean minimizer, Computing and Informatics 22 (2003)
     19–51.
 [9] E. Calò, J. Levy, General boolean formula minimization with QBF solvers, in: Proc. of the 25th
     International Conference of the Catalan Association for Artificial Intelligence, volume 375 of
     Frontiers in Artificial Intelligence and Applications, IOS Press, 2023, pp. 347–358.
[10] J. Marques-Silva, Logic-based explainability in machine learning, in: Proc. of the 18th International
     Summer School 2022 on Reasoning Web. Causality, Explanations and Declarative Knowledge,
     volume 13759 of Lecture Notes in Computer Science, Springer, 2022, pp. 24–104.
[11] T. Lampert, Minimizing disjunctive normal forms of pure first-order logic, Logic Journal of the
     IGPL 25 (2017) 325–347.
[12] P. Blackburn, M. de Rijke, Y. Venema, Modal Logic, volume 53 of Cambridge Tracts in Theoretical
     Computer Science, Cambridge University Press, 2001.
[13] M. Ben-Ari, Z. Manna, A. Pnueli, The temporal logic of branching time, in: Proc. of the 8th Annual
     ACM Symposium on Principles of Programming Languages, ACM Press, 1981, pp. 164–176.
[14] J. Halpern, Y. Shoham, A propositional modal logic of time intervals, J. ACM 38 (1991) 935–962.
[15] A. Pnueli, The temporal logic of programs, in: Proc. of the 18th Annual Symposium on Foundations
     of Computer Science, IEEE Computer Society, 1977, pp. 46–57.
[16] M. Aiello, J. van Benthem, A modal walk through space, Journal of Applied Non Classical Logics
     12 (2002) 319–364.
[17] L. Sikos, Description Logics in Multimedia Reasoning, Springer, 2017.
[18] G. Bechini, E. Losi, L. Manservigi, G. Pagliarini, G. Sciavicco, I. E. Stan, M. Venturini, Statistical
     rule extraction for gas turbine trip prediction, Journal of Engineering for Gas Turbines and Power
     145 (2023) GTP–22–1408.
[19] F. Manzella, G. Pagliarini, G. Sciavicco, I. Stan, The voice of COVID-19: breath and cough recording
     classification with temporal decision trees and random forests, Artificial Intelligence in Medicine
     137 (2023) 102486.
[20] G. Pagliarini, G. Sciavicco, Interpretable land cover classification with modal decision trees,
     European Journal of Remote Sensing 56 (2023) 2262738.
[21] S. Mazzacane, M. Coccagna, F. Manzella, G. Pagliarini, V. Sironi, A. Gatti, E. Caselli, G. Sciavicco,
     Towards an objective theory of subjective liking: A first step in understanding the sense of beauty,
     PLOS ONE (2023) 1–20.
[22] D. Della Monica, G. Pagliarini, G. Sciavicco, I. Stan, Decision trees with a modal flavor, in: Proc.
     of the 21st International Conference of the Italian Association for Artificial Intelligence, volume
     13796 of Lecture Notes in Computer Science, Springer, 2022, pp. 47–59.
[23] R. E. Ladner, The computational complexity of provability in systems of modal propositional logic,
     SIAM Journal on Computing (1977).
[24] M. Fitting, Tableau methods of proof for modal logics, Notre Dame Journal of Formal Logic 13
     (1972) 237–247.
[25] M. F, Single step tableaux for modal logics, Journal of Automatic Reasoning 24 (2000) 319–364.
[26] F. Giunchiglia, R. Sebastiani, Building decision procedures for modal logics from propositional
     decision procedures: The case study of modal k(m), Information and Computation 162 (2000)
     158–178.
[27] C. Areces, R. Gennari, J. Heguiabehere, M. de Rijke, Tree-based heuristics in modal theorem
     proving, in: Proc. of the 14th European Conference on Artificial Intelligence (ECAI), IOS Press,
     2000, pp. 199–203.
[28] G. Pan, U. Sattler, M. Vardi, Bdd-based decision procedures for the modal logic K, Journal of
     Applied Non Classical Logics 16 (2006) 169–208.
[29] R. Sebastiani, A. Tacchella, SAT techniques for modal and description logics, in: Handbook of
     Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications,
     IOS Press, 2021, pp. 1223–1266.
[30] M. Bienvenu, Prime implicates and prime implicants: From propositional to modal logic, J. Artif.
     Intell. Res. (JAIR) (2009).
[31] F. Manzella, G. Pagliarini, A. Paparella, G. Sciavicco, I. Stan, Sole.jl – Symbolic Learning in Julia,
     https://github.com/aclai-lab/Sole.jl, 2024.