One way towards the design of trustable, explainable, and interpretable artificial intelligence models is to focus on symbolic machine learning models, such as decision trees. While decision trees are already intelligible in principle, the logical rules they enclose may still be redundant, in particular with respect to some underlying theory. Moreover, propositional decision trees have been recently generalized to the case of modal logic; modal decision trees turn out to be more expressive than propositional ones, so their corresponding modal rules are proportionally harder to understand and minimize. In this paper we approach the problem of minimizing logical rules extracted from (modal) decision trees modulo some external theory.
Decision trees are part of a collection of logic-based learning methods that include learning
DNF/CNF formulas, Horn formulas, and decision lists, and characterized by the implicit
assumption that each instance of a dataset can be seen as a logical model. Among such methods, decision
trees are probably the most successful one. Learning an optimal decision tree, that is, a decision
tree with a minimum number of nodes, is an Σ 1 -hard problem [
To overcome some of the limitations of propositional decision trees, several generalizations
have been proposed; a very recent one consists of replacing propositional logic with modal
logic [
Since decision tree learning algorithms are sub-optimal, class-formulas may display some kind of redundancy. At the propositional level, for example, a very simple case occurs when a product includes the conjunction of two literals of the type > and > ′, being ≥ ′; clearly, > ′ can be omitted. More generally, one can consider the situation in which a given learning problem is linked to a finite theory , possibly provided by an expert and/or induced by the nature of propositional letters, that may help simplifying the learned model; for example, we may know that > 38 implies ℎ = , so that a term that contains both literals may, again, be simplified. In this paper, we want to define the problem of simplifying class-formulas modulo a theory, and discuss an initial approach to its solution. 2. Minimization of Modal Class-Formulas Modulo Theory Given a (modal) decision tree for a fixed language ℒ and vocabulary , a theory written in the language ℒ, a class , and the class-formula for , we can formulate the problem of Algorithm 1: TheoryMinimize.
function TheoryMinimize(, ):
return TMin(, , ) end function TMin(, , ): if ̸= then if = 1 ∧ 2 then ← (TMin( 1, , ) ∧ TMin( 2, , )) else if = 1 → 2 then ← (TMin( 1, , ) → TMin( 2, , )) else if = ♢ then ← ♢ TMin(, , ) else if = □ then ← □ TMin(, , ) if ̸= 1 ∧ 2 then ← ( ) else if = 1 ∧ 2 and ̸= 1 ∧ 2 then (, ) ← ReplaceMarkedSubFormulasWithNewLetters( ) ′ ← CNFMin( ∧ ) ← ReplaceLettersWithSubFormulas( ′, ) return end ifnding the smallest (in terms of number of symbols) ′ equivalent to in every model in which holds universally; in other words, we ask that for every instance such that for every world it is the case that , ⊩ for each ∈ , it so happens that , 0 ⊩ if and only if , 0 ⊩ ′. In the general case of modal decision trees, class-formulas have the form
( 11 ∧ 21 ∧ . . . ∧ 11 ) ∨ . . . ∨ ( 1 ∧ 2 ∧ . . . ∧ ),
where each (called path-formula) is a formula that belongs to a specific grammar. So, this
problem is at least Σ 2 -hard, as it can be reduced to the propositional DNF minimization with
an empty theory [
A two-step sub-optimal approach towards the solution to the above problem, in the particular case in which only contains propositional implications of the type ( 1 ∧ 2 ∧ . . . ∧ → ) (where and each is a propositional literal); the eficiency of such an approach depends, among other aspects, on the eficiency of the algorithm Norm( ) that, given , returns its logical negation ′ (in the same grammar).
In step one (Alg. 1) we take advantage from the fact that class-formulas present typical patterns for which the theory can be exploited towards a simplification, considering each pathformula of each term ( 1 ∧ 2 ∧ . . . ∧ ) individually. First, the procedure inductively searches for a maximal subtree of the syntax tree of the considered formula that is a conjunction. Then, it substitutes every conjunct that is not a literal with a fresh propositional letter (ReplaceMarkedSubformulasWithNewLetters), using a map to keep trace of each substitution. Finally, it delegates the process of minimizing the size of the obtained conjunctive formula within the theory to an heuristic minimization algorithm CNFMin, before replacing back the fresh letters with the original subtrees (ReplaceLettersWithSubFormulas). The call CNFMin( 1 ∧ 2 ∧ . . . ∧ ∧ ) returns a conjunction 1 ∧ . . . ∧ ( ≤ , 1, . . . , ∈ [1, ]) such that for every with Algorithm 2: PropositionalMinimize.
function PropositionalMinimize( ): (, ) ← ReplaceConjunctsWithNewLiterals( ) ′ ← DNFMin( ) return ReplaceLiteralsWithConjuncts( ′, ) end function ReplaceSubFormulasWithNewLiterals( ): ← ∅ foreach ∈ Conjuncts( ) do if [ ] does not exist then ˜ ← () [ ] ← ˜
˜
[Norm(¬ )] ← ¬
← [ ]
return (, )
end
∈/ {1, . . . , } it is the case that 1 ∧ . . . ∧ ∧ → is valid, and that the subset
{ 1 , . . . , } is minimal. A procedure CNFMin as we have described it can be obtained by
simply adapting a deletion-based procedure, namely, plain deletion-based MES extraction, from [
□ (¬ ∧ ♢ ) ∧ would be reduced to the term if contained the implications ¬ → and ¬ → .
In step two (Alg. 2), we operate on the whole class-formula by uniformly substituting every
(top-level) conjunct in every term of the class-formula being considered with a fresh literal
(ReplaceConjunctsWithNewLiterals), delegating the size minimization of the resulting DNF
formula to a procedure DNFMin [
( 1 ∧ ¬ 2 ∧ 3) ∨ ( 1 ∧ 3)
1 ∧ 3.
We defined the problem of minimization of class-formulas extracted from (modal) decision trees, and we proposed an initial, heuristic approach to its solution.