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 efective 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.
The expressiveness of two-valued Boolean algebra capable of describing switching circuit operations,
highlighted by Shannon in 1938 [
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 [
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 efort by ofering solutions that
are good, though not necessarily optimal and represent local optima. Historically, exact algorithms
have evolved from the foundational Quine-McCluskey algorithm. Notable implementations include
ESPRESSO [
Beyond its foundational application in circuit minimization, propositional minimization finds
relevance 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 [
While minimization has traditionally centered on propositional logic, similar inquiries can be
extended to more expressive logical frameworks. For instance, first-order logic has been explored in this
context [
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.
The syntax of well-formed formulae in the basic modal language [
, 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 diferent, 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 Moreover, we have , |= , |= ¬ , |= ∧ , |= ∨ , |= ♢ , |= □ if if if if if if ∈ (), , ̸|= , , |= and , |= , , |= or , |= , ∃ s.t. and , |= , ∀ s.t. it is the case that , |= .
, |= ⊤, , ̸|= ⊥.
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 PSPACEcomplete [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 [
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 [
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.
(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.
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
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 terminates.
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. □
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. □
It is worth observing that our approach for EXACT-MMEF() is substantially equivalent to the naïve
approach for EXACT-PMEF() as shown in [
Algorithm 2: Heuristic Modal Minimal Equivalent Formula ′ ← HEURISTIC-PMEF(, ) end (, ) ← PROPOREPLACE(NNF ( ′), , − 1, 0, )
Max , ) ⊚ HMMEF( 2, , , ,
Max , )
Max , )
The naïve PSPACE approach to formula minimization, as discussed, exhibits considerable ineficiency. This ineficiency 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 eficient 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 ofers more operational feasibility. Drawing inspiration from [ 26], this approach exploits
eficient 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 [
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, EXACTMMEF() 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 suficiently 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 diferent 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 formula onto which HEURISTIC-MMEF() is called, and that its signature.
with 1 ≤ , , ≤ | |, that Max is the length of the 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, ′ ≡ ¬ ′′), and (ii) if is a literal not in , then ′[ ] exists, (iii) for any pair of formulae ′, ′′, ′[ ′] = ′[ ′′] (resp., ′[ ′] ≡ ¬ ′[ ′′]) implies ′ ≡ ′′ (resp., (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
Max , ): end ˜ ← NEWLETTER()
˜ [ ] ← [NNF (¬ )] ← ¬ ˜ return ([ ], ) if [ ] exists then return ([ ], ) ˜ ← NEWLETTER()
˜ [ ] ← [NNF (¬ )] ← ¬ ˜ return ([ ], ) end else if = ♢ 1 then if | | ≤ then forall ≤ Max do forall ∈ Φ(( )) such that is in NNF and | | = do if EQUIVALENT(, ) and [ ] exists then
return ([ ], ) end else if = 1 ⊚ 2 then ( ′1, 1) ← PROPOREPLACE ( 1, , , Max , ) ( ′2, 2) ← PROPOREPLACE ( 2, , 1, Max , ) return ( ′1 ⊚ ′2, 2) 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(, , ( ′′, ) = PROPOREPLACE( ′, , − 1, Max, ), then ′′ ≡ . ∅, Max, ), ′ = PMEF( ), and 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: ˜ ∈ ′() if ︂{ − 1[˜] = − 1[˜] = ¬ , |= , , ̸|= or 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 diferent 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 diferent 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(, , , and | | ≤ | |. ), then ≡
It is quite trivial to see that HEURISTIC-MMEF() works in polynomial space; however, it is worth discussing its temporal complexity. Let HEURISTIC-MMEF(, , , ) denote the cost of executing HEURISTICMMEF() on a formula of length , with parameters , , and , can be now estimated. A straightforward computation of its growth rate might not yield insightful results due to its heavy dependence 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 worstcase 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 eficient 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( ) + (2PSAT() + 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 (2MSAT()), we have that: HEURISTIC-MMEF(, , ,
) = ((2PSAT() + PMEF() + )) = (2MSAT()), 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 diferent 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.
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 PSPACEcomplete, and we proposed a heuristic algorithm, namely HEURISTIC-MMEF(), for it; we proved the soundness of our proposal, and we discussed its theoretical complexity.
(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. (b) In Step 2, since | | > , a call to HEURISTIC-PMEF() is made resulting in the elimination of 1 from the rightmost conjunct.
(3) =⇒ □ → ∧ ∧ ∧
(4-11) =⇒
∧ □ → ∧ ∧ □ ∧ ♢ ⊤ ⊤ → ♢ (c) In Step (3) a call to PROPREPLACE() operates the back substitution. (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.
The natural continuation of this work is to implement HEURISTIC-MMEF() and to perform a comprehensive test to assess its practical usefulness. Moreover, as it is customary with heuristic solutions, some diferent choices may lead to diferent behaviours in terms of practical eficiency; 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].
This research has been partially funded by the FIRD project Modal Geometric Symbolic Learning (University 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. 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
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.