=Paper=
{{Paper
|id=Vol-3733/paper2
|storemode=property
|title=On Modal Logic Formulae Minimization
|pdfUrl=https://ceur-ws.org/Vol-3733/paper2.pdf
|volume=Vol-3733
|authors=Giovanni Pagliarini,Andrea Paradiso,Guido Sciavicco,Ionel Eduard Stan
|dblpUrl=https://dblp.org/rec/conf/cilc/PagliariniPSS24
}}
==On Modal Logic Formulae Minimization==
https://ceur-ws.org/Vol-3733/paper2.pdf
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.