1 Introduction↩︎

1.0.0.1 Explainability as a query-language problem.

The increasing use of machine learning (ML) models in decision-making systems has created a pressing need for principled methods to understand the predictions produced by such models. This need has led to a large body of work in explainable AI (XAI) [1]–[4], and in particular to a variety of queries, scores, and explanation notions aimed at identifying why a model classifies a given input in a particular way [5]–[7]. Examples include abductive explanations, contrastive explanations, counterfactual-style queries, and feature-necessity or feature-relevance notions [8]–[11].

From a data management perspective, this proliferation of explanation notions suggests a natural question: rather than designing a separate algorithm or formalism for each explanation task, can we develop a declarative language in which users specify what explanation they are looking for? This is in line with a long tradition in databases: complex computational tasks are exposed through query languages with well-defined syntax and semantics, while the study of their expressive power and evaluation complexity provides a principled understanding of what can be asked and how hard it is to answer [12]–[15]. In this view, a model becomes an object over which one poses queries, and explanation notions become fixed queries evaluated over that object [16], [17].

This perspective has several advantages. First, it provides a uniform framework for comparing and combining explanation notions. This is important because there is no single explanation concept that is best suited for all users, models, or applications; in many cases, the most informative explanation is obtained by combining several criteria [18], [19]. Second, it makes it possible to study explainability through standard database-theoretic lenses, such as expressiveness and evaluation complexity [12], [14], [20]. Third, it opens the door to the development of general optimization techniques for the operators of a query language for explainability. Such techniques can reduce the evaluation time of several explainability queries simultaneously, rather than treating each query in isolation.

A central issue in such a framework is how to measure the complexity of query evaluation. Since an explanation notion is intended to be specified by a fixed formula of the language, the appropriate measure is data complexity: the query is fixed, while the input consists of the model representation and the instance to be explained [14]. From this perspective, polynomial-time data complexity is desirable, but it is not the only meaningful tractability target. Many explanation tasks are inherently computationally demanding [21], [22], and therefore a useful explainability language should also allow controlled forms of non-polynomial complexity. In particular, data complexity in \(\mathrm{P}^{\mathrm{NP}}\) remains a reasonable and useful target: it corresponds to computation with a polynomial number of calls to an NP oracle, and it is compatible with the use of SAT solvers as evaluation engines. This complexity level is especially appropriate in our setting because the inputs are model representations, not database instances in the traditional sense. In contrast with large relational databases, the tree-based models commonly considered in formal explainability are often of moderate size, and SAT-based methods have been successfully used to compute explanations for such models [23]–[25]. Thus, in this paper we regard polynomial time and \(\mathrm{P}^{\mathrm{NP}}\) as desirable data-complexity bounds for an explainability query language.

1.0.0.2 Toward declarative languages for model interpretability.

A first step in this direction was taken by Arenas et al. [16], who introduced FOIL, a first-order interpretability logic for querying ML models. FOIL is model-agnostic: it treats a model as a black box and provides access to its positive instances together with the natural subsumption relation over partial instances. This simple design makes FOIL an appealing foundational language, and it is expressive enough to capture several basic explanation notions.

However, model-agnosticism also has limitations. If the language is too weak, it cannot express explanation concepts that are central in practice. If it is too unconstrained, its evaluation problem may become too complex to support query evaluation in the sense expected from a database-oriented framework. Thus, the challenge is to design a language that balances two requirements. On the one hand, it should be expressive enough to capture a broad family of explanation queries, including optimality-based notions such as minimum or maximum explanations. On the other hand, it should have well-behaved evaluation and computation problems over relevant classes of Boolean models.

In this paper, we address this challenge by developing a declarative framework for explaining Boolean models. Our setting is not tied to decision trees. Instead, we consider models abstractly as Boolean functions, while also studying concrete representation classes such as deterministic and decomposable Boolean circuits and decision trees. This allows us to separate the logical specification of explanation queries from the representation-dependent complexity of evaluating them. Such a separation is particularly natural from a database perspective, where query specification and query evaluation over different representation classes are treated as distinct but connected problems.

1.0.0.3 The limitations of FOIL

We begin by revisiting FOIL from the perspective of query-language design. We show that, despite its foundational role, FOIL does not satisfy the requirements above. First, FOIL lacks the expressive power needed to capture some natural optimality-based explanation notions. In particular, we prove that minimum abductive explanations cannot be expressed in FOIL, even when the underlying model is restricted to be a decision tree. This shows that the limitation is not caused by the use of complex model classes, but by the expressive resources of the language itself. Second, FOIL has high evaluation complexity. We prove that, for every level of the polynomial hierarchy, there is a fixed FOIL formula whose evaluation problem over decision trees is hard for that level. Thus, even on a class of models traditionally regarded as interpretable, unrestricted FOIL does not provide the kind of controlled data complexity that one would expect from a practical declarative language for explanations. This complements earlier complexity-theoretic approaches to model interpretability, which study the difficulty of answering explanation queries over different model classes [21], [22].

1.0.0.4 ExplAIner: a tractable logic for explanation queries.

Motivated by these limitations, we introduce ExplAIner, a first-order logic designed to express explanation queries over Boolean models while retaining controlled evaluation complexity. The language extends the basic FOIL vocabulary with a relation that compares partial instances according to the number of defined features. This addition is essential for expressing optimality conditions based on cardinality, such as minimum abductive explanations [9], [21] and maximum contrastive explanations [8], [11].

ExplAIneris organized in layers. Its atomic layer captures structural properties of partial instances; its quantified layer allows formulas to refer to the behavior of the model by combining formulas from the atomic layer with the predicates \(\mathsf{AllPos}\) and \(\mathsf{AllNeg}\), which express whether all completions of a partial instance are classified positively or negatively; and its topmost layer permits Boolean combinations of explanation properties. This organization is designed to provide enough expressive power for explanation tasks while keeping evaluation under control.

We show that ExplAInercan express the explanation notions studied in this paper, including weak abductive explanations, abductive explanations, and minimum abductive explanations [8], [9], [21], [26]; weak contrastive explanations, contrastive explanations, and maximum contrastive explanations [7], [8], [21]; minimum change required and maximum change allowed [21]; and necessary features and relevant features [11], [27]. At the same time, we prove that the evaluation problem for ExplAInerbelongs to the Boolean hierarchy over every class of models for which the basic \(\mathsf{AllPos}\) and \(\mathsf{AllNeg}\) checks are tractable. This includes decision trees and also richer representation classes with suitable tractability properties, such as deterministic and decomposable Boolean circuits [28], [29].

1.0.0.5 Opt-FOIL: computing explanations.

Evaluation is only one part of the problem. A language for explainability should also support the computation of explanations. For this reason, we introduce Opt-FOIL, an optimization-oriented fragment built from the quantified layer of ExplAInertogether with a minimization operator over definable strict partial orders.

Opt-FOILcaptures explanation tasks in which one seeks an object satisfying a logical specification and minimal with respect to a user-defined preference order. This includes standard subset-minimal explanations, cardinality-minimum explanations, and distance-based notions such as minimum change required. By changing the order, the same formalism can also express maximality-based notions, such as maximum contrastive explanations and maximum change allowed.

Our main computational result for Opt-FOILis that its computation problem belongs to \(\mathrm{FP}^{\mathrm{NP}}\) over every class of models for which \(\mathsf{AllPos}\) and \(\mathsf{AllNeg}\) can be evaluated in polynomial time, where \(\mathrm{FP}\) is the class of functions that can be computed in polynomial time. In the terminology above, this means that computing explanations specified in Opt-FOILhas controlled data complexity: the formula is fixed, and the cost is measured as a function of the model representation and the input instance. This places Opt-FOILwithin the complexity regime identified above as suitable for declarative explainability languages, while allowing the language to capture optimization-based explanation tasks that are unlikely to admit polynomial-time algorithms in full generality.

1.0.0.6 Technical contributions.

The following are the technical contributions of the paper.

• We prove two limitations of FOIL over decision trees. On the expressiveness side, we show that no FOIL formula can define the minimum abductive explanation query. On the complexity side, we prove that for every level \(\Sigma_k^P\) of the polynomial hierarchy, there is a fixed FOIL formula whose evaluation problem is \(\Sigma_k^P\)-hard.

• We introduce ExplAIner, a logic based on FOILwith an extended vocabulary and a layered structure: the atomic layer, the quantified layer, and the full ExplAInerlayer. The vocabulary of ExplAInerconsists of the predicates \(\subseteq\), \(\preceq\), \(\mathsf{AllPos}\), and \(\mathsf{AllNeg}\), where \(\subseteq\) is the subsumption relation on partial instances and \(\preceq\) compares partial instances by their number of defined features. We show that both \(\subseteq\) and \(\preceq\) are necessary by proving that neither relation is first-order definable from the other over decision trees.

• We show that ExplAIneris expressive enough to encode the explanation queries considered in the paper, including weak abductive explanations, subset-minimal abductive explanations, cardinality-minimum abductive explanations, weak and maximal contrastive explanations, minimum change required, maximum change allowed, necessary features, and relevant features. Each of these notions is expressed by a fixed query in ExplAIner.

• We establish complexity bounds for the three layers of ExplAIner. First, we show that the evaluation problem for queries in the atomic layer can be solved in polynomial time over every class of Boolean models. Second, for every class of Boolean models over which the predicates \(\mathsf{AllPos}\) and \(\mathsf{AllNeg}\) can be decided in polynomial time, we show that the evaluation problem for queries in the quantified layer is in \({\rm NP}\). Moreover, we show that there exists a query in the quantified layer whose evaluation problem is \({\rm NP}\)-complete over the class of decision trees. Third, for every class of Boolean models over which \(\mathsf{AllPos}\) and \(\mathsf{AllNeg}\) can be decided in polynomial time, we show that the evaluation problem for ExplAInerqueries is in the Boolean hierarchy; equivalently, such queries can be evaluated with a fixed number of calls to an \({\rm NP}\) oracle. Furthermore, we show that for every level \({\rm BH}_k\) of the Boolean hierarchy, there exists an ExplAInerquery whose evaluation problem is \({\rm BH}_k\)-hard over the class of decision trees.

  Importantly, the assumption that the predicates \(\mathsf{AllPos}\) and \(\mathsf{AllNeg}\) can be decided in polynomial time is not specific to decision trees. This condition also holds for more general classes of Boolean models, including deterministic and decomposable Boolean circuits. Thus, the upper bounds above apply beyond tree-based representations and cover circuit classes that are central in knowledge compilation [28].

• We define Opt-FOILas an optimization-oriented fragment of ExplAIner, based on the quantified layer together with a minimization operator over strict partial orders. For every class of Boolean models over which the predicates \(\mathsf{AllPos}\) and \(\mathsf{AllNeg}\) can be decided in polynomial time, we show that the computation problem for Opt-FOILqueries is in \(\mathrm{FP}^{\mathrm{NP}}\). Hence, explanations specified in Opt-FOILcan be computed with a polynomial number of calls to an \({\rm NP}\) oracle.

• As a result of independent interest, we use Presburger arithmetic to show that the problem of verifying whether a sentence over the atomic layer of ExplAIneris valid is decidable. This result is needed to provide an effective syntax for Opt-FOIL, since Opt-FOILrequires verifying that a sentence in the atomic layer defines a strict partial order.

• Finally, we show that, under standard complexity-theoretic assumptions, Opt-FOILis strictly contained in ExplAIner, and ExplAIner is strictly contained in FOILover the extended vocabulary consisting of the predicates \(\subseteq\), \(\preceq\), \(\mathsf{AllPos}\), and \(\mathsf{AllNeg}\).

1.0.0.7 Organization of the paper.

The remainder of the paper is organized as follows. Section 2 introduces the basic notions used throughout the paper, including Boolean models, partial instances, model representations, and the explanation queries studied in our framework. Section 3 revisits \(\mathrm{\small FOIL}\) and establishes its limitations in terms of expressiveness and evaluation complexity. Section 4 introduces ExplAInerand proves its main expressiveness and evaluation results. Section 5 presents Opt-FOIL, our optimization-oriented language for computing explanations, together with its computational guarantees. Section 6 presents concluding remarks and directions for future work. Finally, the appendix contains supplementary material, including technical proofs that are deferred for readability.

2 Background↩︎

We begin by introducing the main components of our framework, followed by a review of various explainability queries that will be addressed in the subsequent sections.

2.1 Models and instances↩︎

We use an abstract notion of a model of dimension \(n\), and define it as a Boolean function \(\mathcal{M}: \{0,1\}^n \to \{0, 1\}\).¹ We write \({\textit dim}(\mathcal{M})\) for the dimension of a model \(\mathcal{M}\). A partial instance of dimension \(n\) is a tuple \(\mathbf{e}\in \{0,1,\bot\}^n\), where \(\bot\) is used to represent undefined features. We define \(\mathbf{e}_\bot = \{i \in \{1,\dots,n\} \mid \mathbf{e}[i] = \bot\}\). An instance of dimension \(n\) is a tuple \(\mathbf{e}\in \{0,1\}^n\), that is, a partial instance without undefined features. For every instance \(\mathbf{e}\) of dimension \({\textit dim}(\mathcal{M})\), we write \(\mathcal{M}(\mathbf{e})\) for the value assigned by \(\mathcal{M}\) to \(\mathbf{e}\).

Given two partial instances \(\mathbf{e}\), \(\mathbf{e}'\) of dimension \(n\), we write \(\mathbf{e}\subseteq \mathbf{e}'\) and say that \(\mathbf{e}\) is subsumed by \(\mathbf{e}'\) if and only if, for every \(i \in \{1, \ldots, n\}\), whenever \(\mathbf{e}[i] \neq \bot\), we have \(\mathbf{e}[i] = \mathbf{e}'[i]\). In other words, \(\mathbf{e}'\) can be obtained from \(\mathbf{e}\) by replacing some occurrences of \(\bot\) by Boolean values. For example, \((1,\bot)\) is subsumed by \((1,0)\), but it is not subsumed by \((0,0)\). A partial instance \(\mathbf{e}\) can be seen as a compact representation of the set of instances \(\mathbf{e}'\) such that \(\mathbf{e}\) is subsumed by \(\mathbf{e}'\). Such instances \(\mathbf{e}'\) are called the completions of \(\mathbf{e}\) and the set of all of them is denoted by \(\textit{comp}(\mathbf{e})\).

For each \(n\), partial instances of dimension \(n\) are partitioned into \(n+1\) levels: for each \(i \in \{0, \ldots, n\}\), level \(i\) consists of all partial instances with exactly \(i\) defined features. Given partial instances \(\mathbf{e}\), \(\mathbf{e}'\), we write \(\mathbf{e}\preceq\mathbf{e}'\) and say that \(\mathbf{e}\) is on a less or equal level than \(\mathbf{e}'\) if and only if \(|\mathbf{e}_\bot| \geq |\mathbf{e}'_\bot|\). In other words, \(\mathbf{e}'\) has at least as many defined features as \(\mathbf{e}\).

We will also use the symbols \(\subset\) and \(\prec\) for the corresponding strict relations.

In several proofs, we write \(\mathbf{e}\cdot \mathbf{e}'\) for the concatenation of both instances. Moreover, for a value \(s \in \{0,1,\bot\}\), we denote by \(\{s\}^{n}\) the partial instance of dimension \(n\) whose entries are all equal to \(s\).

We next introduce several classes of Boolean functions that will be used throughout the paper.

2.1.0.1 Boolean Circuits.

A Boolean circuit of dimension \(n\) is a directed acyclic graph over a set of variables \(\{x_1, ..., x_n\}\) such that:

1. Every node without incoming edges is either a variable gate or a constant gate. A variable gate is labeled with a variable, and a constant gate is labeled with either \(0\) or \(1\);

2. Every node with incoming edges is a logic gate, and is labeled with a symbol \(\land\), \(\lor\) or \(\lnot\). If it is labeled with the symbol \(\lnot\), then it has exactly one incoming edge;

3. Exactly one node does not have any outgoing edges, and this node is called the output gate.

Given a Boolean circuit \(C\) and an instance \(\mathbf{e}\) of dimension \(n\), the value \(C(\mathbf{e})\) is defined as the value of the output gate of \(C\) when we evaluate \(C\) on input \(\mathbf{e}\). Note that we are identifying inputs of the circuit as instances of the Boolean model.

Several restrictions of Boolean circuits with good computational properties have been studied.

2.1.0.2 Negation Normal Form.

A negation normal form (\(\mathsf{NNF}\)) circuit of dimension \(n\) is a Boolean circuit of dimension \(n\) such that the incoming edge of every negation gate comes from a variable gate.

2.1.0.3 Determinism and decomposability.

Let \(X\) be a set of variables, let \(C\) be a circuit over \(X\), and let  \(g\) be a gate of \(C\). We define \(C_g\) to be the Boolean circuit over \(X\) induced by the set of gates \(g'\) of \(C\) for which there exists a directed path from \(g'\) to \(g\) in \(C\). Note that \(g\) is the output gate of \(C_g\). An \(\lor\)-gate \(g\) of \(C\) is said to be deterministic if, for every pair \(g_1\), \(g_2\) of distinct input gates of \(g\), there is no instance \(\mathbf{e}\) such that \(C_{g_1}(\mathbf{e}) = C_{g_2}(\mathbf{e}) = 1\). The circuit \(C\) is called deterministic if every \(\lor\)-gate of \(C\) is deterministic. For every gate \(g\) of \(C\), define \(\mathsf{var}(g)\) as the set of variables \(x \in X\) such that there exists a variable gate labeled by \(x\) in \(C_g\). An \(\land\)-gate \(g\) of \(C\) is said to be decomposable if for every pair \(g_1\), \(g_2\) of distinct input gates of \(g\), we have \(\mathsf{var}(g_1) \cap \mathsf{var}(g_2) = \emptyset\). The circuit \(C\) is called decomposable if every \(\land\)-gate of \(C\) is decomposable.

2.1.0.4 Deterministic Decomposable Negation Normal Form.

A deterministic decomposable negation normal form (\(\mathsf{d}\text{-}\mathsf{DNNF}\)) circuit of dimension \(n\) is an \(\mathsf{NNF}\) circuit of dimension \(n\) that is both deterministic and decomposable. An example is shown in [fig:ddnnf].

2.1.0.5 Binary Decision Diagram.

A binary decision diagram (\(\mathsf{BDD}\)) of dimension \(n\) is a directed acyclic graph with a unique root, and whose nodes and edges are labeled as follows: (i) every leaf is labeled by \(\mathbf{true}\) or \(\mathbf{false}\) and (ii) every non-leaf node is labeled by a feature in \(\{1, ..., n\}\) and has exactly two outgoing edges, one labeled by \(0\) and the other by \(1\).

Let \(B\) be a binary decision diagram and let \(\mathbf{e}\) be an instance of dimension \(n\). The value \(B(\mathbf{e})\) is defined as the Boolean value of the leaf obtained by starting at the root and following the path such that, at each non-leaf node labeled by \(i\), the outgoing edge labeled by \(\mathbf{e}[i]\) is chosen.

2.1.0.6 Decision Trees.

A decision tree (\(\mathsf{DTree}\)) over instances of dimension \(n\) is a binary decision diagram of dimension \(n\) such that (i) its underlying graph is a tree and (ii) no feature appears more than once on any root-to-leaf path. An example is shown in [fig:dtree].

2.2 Explainability queries↩︎

We now define the explainability queries studied in this work.

2.2.0.1 Weak Abductive Explanation.

Given an instance \(\mathbf{e}\) and a model \(\mathcal{M}\), a partial instance \(\mathbf{e}_1\) is a weak abductive explanation (\(\mathsf{wAXp}\)) for \(\mathbf{e}\) on \(\mathcal{M}\) if \(\mathbf{e}_1 \subseteq \mathbf{e}\) and, for every \(\mathbf{e}_2 \in \textit{comp}(\mathbf{e}_1)\), the condition \(\mathcal{M}(\mathbf{e})=\mathcal{M}(\mathbf{e}_2)\) holds [11]. This notion is also known as sufficient reason in the literature [32]. For example, in [fig:ddnnf], \((1,1,1,\bot)\) is a weak abductive explanation for the instance \((1,1,1,1)\).

2.2.0.2 Abductive Explanation.

Given a pair \((\mathbf{e},\mathcal{M})\), a partial instance \(\mathbf{e}_1\) is an abductive explanation (\(\mathsf{AXp}\)) for \(\mathbf{e}\) on \(\mathcal{M}\) if it is a weak abductive explanation for \(\mathbf{e}\) on \(\mathcal{M}\) and there is no weak abductive explanation \(\mathbf{e}_2\) such that \(\mathbf{e}_2 \subset \mathbf{e}_1\) [8]. This notion of explanation has been extensively studied and it can be found in the literature under names such as sufficient reason [9], [33], prime implicant [34], and minimal sufficient reason [32]. Modeling abduction using propositional logic or first-order logic, and the complexity of computing such an explanation has been studied for many decades [35]. In [fig:ddnnf], \((1,1,1,\bot)\) is a weak abductive explanation for \((1,1,1,1)\), but not an abductive explanation. By contrast, one can check that \((1,1,\bot,\bot)\) is indeed an abductive explanation.

2.2.0.3 Minimum Abductive Explanation.

Given a pair \((\mathbf{e},\mathcal{M})\), a partial instance \(\mathbf{e}_1\) is a minimum abductive explanation (\(\mathsf{mAXp}\)) for \(\mathbf{e}\) on \(\mathcal{M}\) if it is a weak abductive explanation for \(\mathbf{e}\) on \(\mathcal{M}\) and there is no weak abductive explanation \(\mathbf{e}_2\) such that \(\mathbf{e}_2 \prec\mathbf{e}_1\). Our definition is based on the minimum sufficient reason explainability query by [21] and [32]. In [fig:ddnnf], \((1,1,\bot,\bot)\) is also a minimum abductive explanation for \((1,1,1,1)\).

2.2.0.4 Weak Contrastive Explanation.

Given a pair \((\mathbf{e},\mathcal{M})\), the partial instance \(\mathbf{e}_1\) is a weak contrastive explanation (\(\mathsf{wCXp}\)) for \(\mathbf{e}\) on \(\mathcal{M}\) if \(\mathbf{e}_1 \subseteq \mathbf{e}\) and there is an instance \(\mathbf{e}_2 \in \textit{comp}(\mathbf{e}_1)\) such that the condition \(\mathcal{M}(\mathbf{e})\not =\mathcal{M}(\mathbf{e}_2)\) holds [6].

2.2.0.5 Contrastive Explanation.

Given a pair \((\mathbf{e},\mathcal{M})\), the partial instance \(\mathbf{e}_1\) is a contrastive explanation (\(\mathsf{CXp}\)) for \(\mathbf{e}\) on \(\mathcal{M}\) if it is a weak contrastive explanation for \(\mathbf{e}\) on \(\mathcal{M}\) such that there is no weak contrastive explanation \(\mathbf{e}_2\) satisfying \(\mathbf{e}_1 \subset \mathbf{e}_2\). It can be shown that this definition is equivalent to the one by [6].

2.2.0.6 Maximum Contrastive Explanation.

Given a pair \((\mathbf{e},\mathcal{M})\), the partial instance \(\mathbf{e}_1\) is a maximum contrastive explanation (\(\mathsf{mCXp}\)) for \(\mathbf{e}\) on \(\mathcal{M}\) if it is a weak contrastive explanation for \(\mathbf{e}\) on \(\mathcal{M}\) such that there is no weak contrastive explanation \(\mathbf{e}_2\) satisfying \(\mathbf{e}_1 \prec\mathbf{e}_2\). In [fig:ddnnf], the partial instance \((\bot,1,1,1)\) is a maximum contrastive explanation for \((1,1,1,1)\), thus also a \(\mathsf{CXp}\) and a \(\mathsf{wCXp}\).

2.2.0.7 Minimum Change Required.

Given a pair \((\mathbf{e},\mathcal{M})\), an instance \(\mathbf{e}_1\) is a solution to the minimum change required query (\(\mathsf{MCR}\)) for \(\mathbf{e}\) on \(\mathcal{M}\) if \(\mathcal{M}(\mathbf{e}) \not = \mathcal{M}(\mathbf{e}_1)\) and \(\mathcal{M}(\mathbf{e}) = \mathcal{M}(\mathbf{e}_2)\), for every instance \(\mathbf{e}_2\) at smaller Hamming distance (meaning the number of flipped features between two instances) from \(\mathbf{e}\) than \(\mathbf{e}_1\). The instance \(\mathbf{e}_1\) represents the minimum distance required to change the value on the model. This notion is based on the query introduced by [21]. Considering the instance \((1,1,1,1)\) in [fig:ddnnf], one possible explanation for the query is \((0,1,1,1)\).

2.2.0.8 Maximum Change Allowed.

Given a pair \((\mathbf{e},\mathcal{M})\), an instance \(\mathbf{e}_1\) is a solution to the maximum change allowed query (\(\mathsf{MCA}\)) for \(\mathbf{e}\) on \(\mathcal{M}\) if \(\mathcal{M}(\mathbf{e}) = \mathcal{M}(\mathbf{e}_1)\) and \(\mathcal{M}(\mathbf{e}) \not = \mathcal{M}(\mathbf{e}_2)\), for every instance \(\mathbf{e}_2\) at greater Hamming distance from \(\mathbf{e}\) than \(\mathbf{e}_1\). This notion is based on the query introduced by [36]. As the authors argue, only studying counterfactual queries like minimum change required may not capture the whole picture for explaining certain situations. That is why we include their semifactual version of the problem. In [fig:ddnnf], the maximum change allowed for the negative input \((0,1,1,1)\) is the instance \((0,0,0,0)\).

The original versions of \(\mathsf{MCR}\) and \(\mathsf{MCA}\) [21], [36] are defined similarly with respect to each other, but have very different interpretations. Given a distance \(k\) for \(\mathsf{MCR}\) it is not trivially easier to decide any distance \(k'\) for \(\mathsf{MCA}\); and vice versa. We only know that the inequality \(k \leq k' + 1\) holds. Thus, presenting both queries has additional value and lets us present another useful case of maximization.

2.2.0.9 Necessary Feature.

Given a pair \((\mathbf{e},\mathcal{M})\), a partial instance \(\mathbf{e}_1\) with exactly one defined feature is a necessary feature (\(\mathsf{NF}\)) for \(\mathbf{e}\) on \(\mathcal{M}\) if, for every weak abductive explanation \(\mathbf{e}_2\) for \(\mathbf{e}\) on \(\mathcal{M}\), \(\mathbf{e}_1 \subseteq \mathbf{e}_2\) holds. An equivalent formulation appears in [11], where the authors define the property feature necessity on their own framework using abductive explanations instead of weak abductive explanations. It is easy to see that both definitions are equivalent. Considering \((1,1,1,1)\) in [fig:ddnnf], the instance has two abductive explanations: \((1,1,\bot,\bot)\) and \((1,\bot,1,1)\). Therefore, the feature \(x_1=1\), represented by the partial instance \((1,\bot,\bot,\bot)\), is a necessary feature.

2.2.0.10 Relevant Feature.

Given a pair \((\mathbf{e},\mathcal{M})\), a partial instance \(\mathbf{e}_1\) with exactly one defined feature is a relevant feature (\(\mathsf{RF}\)) for \(\mathbf{e}\) on \(\mathcal{M}\) if there exists an abductive explanation \(\mathbf{e}_2\) for \(\mathbf{e}\) on \(\mathcal{M}\) such that \(\mathbf{e}_1 \subseteq \mathbf{e}_2\). This notion appears in the literature as the AXp membership problem [37] and as feature relevancy [11]. Considering \((1,1,1,1)\) and its abductive explanations \((1,1,\bot,\bot)\) and \((1,\bot,1,1)\) in [fig:ddnnf], \(x_2=1\) is one of the relevant features, and can be represented by the partial instance \((\bot,1,\bot,\bot)\).

3 First Order Interpretability Logic↩︎

In this section, we introduce an initial interpretability logic designed for expressing queries. We demonstrate that it faces limitations in expressive power and exhibits high computational complexity for its evaluation problem.

Our work is inspired by the first-order interpretability logic (\(\mathrm{\small FOIL}\)) [16], which is a simple explainability language rooted in first-order logic. \(\mathrm{\small FOIL}\) is simply first-order logic over two relations on the set of partial instances of a given dimension: a unary relation \(\mathsf{Pos}\) whose interpretation is the set of instances that are positively classified by the model, and a binary relation \(\subseteq\) that represents the subsumption relation among partial instances.

Given a vocabulary \(\sigma\) consisting of relations \(R_1\), \(\ldots\), \(R_\ell\), recall that a structure \(\mathfrak{A}\) over \(\sigma\) consists of a domain over which quantifiers range, and an interpretation for each relation \(R_i\). Moreover, given a first-order formula \(\varphi\) defined over the vocabulary \(\sigma\), we write \(\varphi(x_1, \ldots, x_k)\) to indicate that the free variables of \(\varphi\) are among \(\{x_1,\ldots,x_k\}\). Finally, given a structure \(\mathfrak{A}\) over the vocabulary \(\sigma\) and elements \(a_1\), \(\ldots\), \(a_k\) in the domain of \(\mathfrak{A}\), we use \(\mathfrak{A}\models \varphi(a_1, \ldots, a_k)\) to indicate that the formula \(\varphi\) is satisfied by \(\mathfrak{A}\) when each variable \(x_i\) is replaced by element \(a_i\) (\(1 \leq i \leq k\)).

Consider a model \(\mathcal{M}\) with \({\textit dim}(\mathcal{M}) = n\). The structure \(\mathfrak{A}_\mathcal{M}\) representing \(\mathcal{M}\) over the vocabulary formed by \(\mathsf{Pos}\) and \(\subseteq\) is defined as follows. The domain of \(\mathfrak{A}_\mathcal{M}\) is the set \(\{0,1, \bot\}^n\) of all partial instances of dimension \(n\). A partial instance \(\mathbf{e}\in \{0,1, \bot\}^n\) belongs to the interpretation of \(\mathsf{Pos}\) in \(\mathfrak{A}_\mathcal{M}\) if and only if \(\mathbf{e}\in \{0,1\}^n\) and \(\mathcal{M}(\mathbf{e}) = 1\). Moreover, a pair \((\mathbf{e}_1,\mathbf{e}_2)\) is in the interpretation of relation \(\subseteq\) in \(\mathfrak{A}_\mathcal{M}\) if and only if \(\mathbf{e}_1\) is subsumed by \(\mathbf{e}_2\). Finally, given a formula \(\varphi(x_1, \ldots, x_k)\) in \(\mathrm{\small FOIL}\) and partial instances \(\mathbf{e}_1\), \(\ldots\), \(\mathbf{e}_k\) of dimension \(n\), the model \(\mathcal{M}\) is said to satisfy \(\varphi(\mathbf{e}_1, \ldots, \mathbf{e}_k)\), denoted by \(\mathcal{M}\models \varphi(\mathbf{e}_1, \ldots, \mathbf{e}_k)\), if \(\mathfrak{A}_\mathcal{M}\models \varphi(\mathbf{e}_1, \ldots, \mathbf{e}_k)\).

Notice that for a succinctly-represented model \(\mathcal{M}\), the structure \(\mathfrak{A}_\mathcal{M}\) can be exponentially larger than the representation of \(\mathcal{M}\). Hence, \(\mathfrak{A}_\mathcal{M}\) is a theoretical construction needed to formally define the semantics of \(\mathrm{\small FOIL}\), but it should not be constructed explicitly when checking in practice if a formula \(\varphi\) is satisfied by \(\mathcal{M}\).

3.1 Expressing interpretability queries in FOIL↩︎

It will be instructive for the rest of our presentation to see a few examples of how \(\mathrm{\small FOIL}\) can be used to express some natural explainability queries on models. In these examples, we make use of the following \(\mathrm{\small FOIL}\) formula: \[\mathsf{Full}(x) \;:= \;\forall y \, (x \subseteq y \, \rightarrow \, y \subseteq x).\]Notice that if \(\mathcal{M}\) is a model and \(\mathbf{e}\) is a partial instance, then \(\mathcal{M}\models \mathsf{Full}(\mathbf{e})\) if and only if \(\mathbf{e}\) is also an instance (i.e., it has no undefined features). We also use the formula \[\mathsf{AllPos}(x) \;:= \;\forall y \, \big((x \subseteq y \wedge \mathsf{Full}(y)) \, \rightarrow \, \mathsf{Pos}(y)\big),\] such that \(\mathcal{M}\models \mathsf{AllPos}(\mathbf{e})\) if and only if every instance in \(\textit{comp}(\mathbf{e})\) is classified as positive by \(\mathcal{M}\). Analogously, we define a formula \(\mathsf{AllNeg}(x)\). The definitions of both predicates are inspired by important knowledge compilation queries such as a conditioning transformation of the input and a consistency or validity check on the conditioned model [28]. \(\mathsf{AllPos}(x)\) and \(\mathsf{AllNeg}(x)\) will be important components of a new logic for explainability defined in 4 since they enable the expression of a wide range of explainability queries. For example, we can now define weak abductive explanations (refer to 2.2) in \(\mathrm{\small FOIL}\) as follows: \[\mathsf{wAXp}(x,y) := \mathsf{Full}(x) \wedge y \subseteq x \;\wedge \\ (\mathsf{Pos}(x) \to \mathsf{AllPos}(y)) \wedge (\neg \mathsf{Pos}(x) \to \mathsf{AllNeg}(y)).\]

In fact, it is easy to see that \(\mathcal{M}\models \mathsf{wAXp}(\mathbf{e},\mathbf{e}')\) if and only if \(\mathbf{e}'\) is a weak abductive explanation for \(\mathbf{e}\) over \(\mathcal{M}\). Notice that \(\mathbf{e}\) is always a weak abductive explanation for itself. However, we are typically interested in explanations that satisfy some optimality criterion. A common such criterion is that of being minimal [21], [34], [38]. Let us write \(x \subset y\) for \(x \subseteq y \wedge \neg (y \subseteq x)\). Then, for \[\mathsf{AXp}(x,y) := \mathsf{wAXp}(x,y) \land \forall z \,(z \subset y \, \rightarrow \neg \mathsf{wAXp}(x,z)),\]we have that \(\mathcal{M}\models \mathsf{AXp}(\mathbf{e},\mathbf{e}')\) if and only if \(\mathbf{e}'\) is an abductive explanation for \(\mathbf{e}\) over \(\mathcal{M}\). We could similarly express local explainability queries like contrastive explanations through the same approach using \(\mathrm{\small FOIL}\).

As we show below, \(\mathrm{\small FOIL}\) fails to meet either of the two criteria we are looking for in a practical language that provides explanations. The first issue is its limited expressiveness: there are important notions of explanations that cannot be expressed in this language, even when restricted to decision trees, which are traditionally deemed to be easily interpretable. The second issue is its high computational complexity: there are queries in \(\mathrm{\small FOIL}\) that cannot be evaluated with a polynomial number of calls to an NP oracle. Both facts firmly establish the inadequacy of \(\mathrm{\small FOIL}\) as a practical language.

3.2 FOIL presents limited expressiveness↩︎

In some scenarios we want to express a stronger condition for abductive and contrastive explanations: not only that they are minimal, but also that they are minimum (see 2.2). In the case of abductive explanations, they can be minimal without being minimum. The following theorem shows that \(\mathrm{\small FOIL}\) cannot express the query that asks whether a partial instance \(\mathbf{e}'\) is a minimum abductive explanation for a given instance \(\mathbf{e}\) over decision trees.

3.3 Evaluating FOIL is intractable↩︎

For each query \(\varphi(x_1, \ldots, x_k)\) in \(\mathrm{\small FOIL}\) and \(\mathcal{C}\) a class of models, we define its associated problem Eval\((\varphi, \mathcal{C})\) as follows (we assume models and instances have the same dimension):

It is known that there exists a formula \(\varphi(x)\) in \(\mathrm{\small FOIL}\) for which its evaluation problem over the class of decision trees is \({\rm NP}\)-hard [16]. We want to determine whether the language \(\mathrm{\small FOIL}\) is appropriate for implementation using SAT encodings. Thus, it is natural to ask whether the evaluation problem for formulas in this logic can always be decided in polynomial time by using a \({\rm NP}\) oracle. However, we prove that this is not always the case. Although the evaluation of \(\mathrm{\small FOIL}\) formulas is always in the polynomial hierarchy (PH), there exist formulas in \(\mathrm{\small FOIL}\) for which their corresponding evaluation problems are hard for every level of PH. Based on widely held complexity assumptions, we can conclude that \(\mathrm{\small FOIL}\) contains formulas whose evaluations cannot be decided in polynomial time by using a \({\rm NP}\) oracle even on decision trees (\(\mathsf{DTree}\)).

4 ExplAIner: a tractable logic for explainability↩︎

In the previous section we identified two limitations of \(\mathrm{\small FOIL}\) that must be addressed in order to build a practical logic for explanations. On one hand, we must extend \(\mathrm{\small FOIL}\) to increase its expressive power, and on the other hand, we must constrain the resulting logic to ensure that its evaluation complexity is appropriate. In this section we define ExplAIner, a logic that takes both criteria into account and in which explainability notions can be expressed naturally.

4.1 The atomic layer of ExplAIner↩︎

\(\mathrm{\small FOIL}\) cannot express properties such as minimum abductive explanations that involve comparing cardinalities of sets of features. As a first step, we solve this issue by extending the vocabulary of \(\mathrm{\small FOIL}\) with a simple binary relation \(\preceq\) defined as: \[\mathcal{M}\models \mathbf{e}\preceq\mathbf{e}' \;\;\Longleftrightarrow \;\; |\mathbf{e}_\bot| \geq |\mathbf{e}'_\bot|.\] As we will show later, the use of this predicate indeed allows us to express many notions of explanations. Note that we could not simply keep only one of \(\subseteq\) and \(\preceq\) when defining the new logic, as we show that they cannot be defined in terms of each other. First, we show that predicate \(\preceq\) cannot be defined in terms of predicate \(\subseteq\).

Second, we show that predicate \(\subseteq\) cannot be defined in terms of predicate \(\preceq\).

However, adding \(\preceq\) to \(\mathrm{\small FOIL}\) can only add extra complexity. Therefore, our second step is to define the logic \(\mathrm{\small ExplAIner}\) expressive enough to capture important notions, but keeping the evaluation tractable using \(\mathrm{\small SAT}\) solvers. Our logic \(\mathrm{\small ExplAIner}\) consists of three hierarchical layers, where the first layer does not depend on the structure of the model.

Predicates \(\subseteq\) and \(\preceq\), as well as predicate \(\mathsf{Full}\) used in Section 3.1, can be regarded as syntactic in the sense that they refer to the values of the features of partial instances, and they do not make reference to classification models. It turns out that all the syntactic predicates needed in our logical formalism can be expressed as first-order formulas over the predicates \(\subseteq\) and \(\preceq\). The atomic formulas of \(\mathrm{\small ExplAIner}\) are defined as first-order formulas over the vocabulary \(\{\subseteq, \preceq\}\). We now prove that such formulas can be evaluated in polynomial time. We also prove that in the case of sentences, that is, formulas without free variables, it is decidable whether a sentence is true in every structure \(\mathfrak{B}_n\).

Given \(n \geq 0\) and a model \(\mathcal{M}\) of dimension \(n\), define \(\mathfrak{B}_\mathcal{M}\) as a structure over the vocabulary \(\{\subseteq, \preceq\}\) generated from \(\mathfrak{A}_\mathcal{M}\) by removing the interpretation of predicate \(\mathsf{Pos}\), and adding the interpretation of predicate \(\preceq\). Notice that, given two models \(\mathcal{M}_1\) and \(\mathcal{M}_2\) of dimension \(n\), we have that \(\mathfrak{B}_{\mathcal{M}_1} = \mathfrak{B}_{\mathcal{M}_2}\), so we define simply \(\mathfrak{B}_n\) as \(\mathfrak{B}_\mathcal{M}\) for an arbitrary model of dimension \(n\). Therefore, when measuring the complexity of evaluating formulas in the atomic layer, we take \(n\) in unary as part of the input, since \(n\) is the size of the partial instances. Hence, for each formula \(\varphi(x_1, \ldots, x_k)\) in the atomic layer of \(\mathrm{\small ExplAIner}\), we define its associated problem Eval\((\varphi)\) as follows:

Recall also that the width of a first-order formula \(\varphi\), denoted \(\rm{wd}(\varphi)\), is defined as the maximum number of free variables among all subformulas of \(\varphi\) (see [39] for a reference).

4.2 The quantified layer of ExplAIner↩︎

In this layer we introduce predicates whose interpretation does depend on the model. The vocabulary of this layer is \(\{\subseteq, \preceq, \mathsf{AllPos}, \mathsf{AllNeg}\}\), where \(\mathcal{M}\models \mathsf{AllPos}(\mathbf{e})\) if and only if all instances in \(\textit{comp}(\mathbf{e})\) are classified positively by \(\mathcal{M}\), and \(\mathsf{AllNeg}\) is defined analogously. As we will show, at this point we will already be able to express properties over polynomial-size sets of instances and minimality/minimum conditions.

We will need two auxiliary formulas from the atomic layer that we already defined during the proof of Theorem 2. The first is \[{\sf Undef}(x) := \neg \exists y (y \subset x),\] which defines the set that only contains the partial instance \(\{\bot\}^{n}\). The second is \[{\sf Single}(x) := \exists y (y \subset x) \wedge \forall y (y \subset x \, \rightarrow \, {\sf Undef}(y)),\] which defines the set of partial instances with exactly one defined feature.

The quantified layer is recursively defined as follows:

1. Boolean combinations of formulas from the atomic layer, together with \(\mathsf{AllPos}(x)\) and \(\mathsf{AllNeg}(x)\), are formulas from the quantified layer.

2. If \(\varphi\) is a formula from the quantified layer, then \(\exists x\;\varphi\) is a formula from the quantified layer.

3. If \(\varphi\) is a formula from the quantified layer, then \(\forall x\;\left( {\sf Single}(x) \to \varphi\right)\) is a formula from the quantified layer.

Using only the first rule we can already express some basic explainability properties. For example, we can express the query for weak abductive explanations as follows: \[\mathsf{wAXp}(x, y) := \mathsf{Full}(x) \wedge y \subseteq x \wedge (\mathsf{AllPos}(x) \to \mathsf{AllPos}(y)) \wedge (\mathsf{AllNeg}(x) \to \mathsf{AllNeg}(y)).\]

The third rule involves the concept of guarded quantification. In that case we only quantify over partial instances with exactly one defined feature, which naturally correspond to assignments of a value to a single feature. On any class of models \(\mathcal{C}\), the number of partial instances with one defined feature is at most twice the dimension of the model, so we cannot express universal properties over superpolynomial-size sets of partial instances. Notice that our rules do not allow us to define unguarded universal quantifiers because the first rule only allows us to take Boolean combinations of unquantified formulas. In particular, in this layer we are not allowed to negate formulas that were produced using the second (or third) rule.

4.3 The ExplAIner logic↩︎

We define \(\mathrm{\small ExplAIner}\) as the logic obtained by taking Boolean combinations of formulas from the quantified layer. In particular, since we can negate quantified formulas, in this third layer we are allowed to use unguarded universal quantifiers. Nevertheless, notice that a necessary condition for a formula to have a valid syntax according to the \(\mathrm{\small ExplAIner}\) logic is that alternations between unguarded quantifiers cannot occur.

We now provide a precise characterization of the complexity of the evaluation problem for \(\mathrm{\small ExplAIner}\). More specifically, we establish that this problem can always be solved in the Boolean Hierarchy over \({\rm NP}\) [42], [43], i.e., in the class consisting of Boolean combinations of \({\rm NP}\) languages. In fact, we will show that the \(\mathrm{\small ExplAIner}\) logic captures the entire Boolean Hierarchy.

For the following theorem, we denote the levels of the Boolean Hierarchy by \({\rm BH}_k\), and we denote by \({\rm BH}\) the Boolean Hierarchy consisting of all these levels.

This result tells us that \(\mathrm{\small ExplAIner}\) meets one of the fundamental criteria for an interpretability logic, namely that we can evaluate an \(\mathrm{\small ExplAIner}\) formula over a tuple of partial instances in polynomial time with a polynomial number of calls to an \({\rm NP}\) oracle. In fact, by definition of the Boolean hierarchy, the evaluation of a fixed \(\mathrm{\small ExplAIner}\) formula can be done with a constant number of calls to an \({\rm NP}\) oracle. Thus, we argue that the technology of \(\mathrm{\small SAT}\) solvers will allow us to tractably evaluate \(\mathrm{\small ExplAIner}\) over classes that support consistency and validity checks in polynomial time. More precisely, Theorem 7 requires the class of models \(\mathcal{C}\) to satisfy that Eval\((\mathsf{AllPos}(x), \mathcal{C}) \in {\rm P}\) and Eval\((\mathsf{AllNeg}(x), \mathcal{C}) \in {\rm P}\) in order for \(\mathrm{\small ExplAIner}\) to be able to tractably solve its evaluation problem over that class. This includes decision trees, but also richer representation classes like \(\mathsf{d}\text{-}\mathsf{DNNF}\) circuits. Moreover, this includes fragments of the class of circuits corresponding to propositional formulas in conjunctive normal form (\(\mathsf{CNF}\)) whose satisfiability can be decided in polynomial time, such as the class of circuits corresponding to CNF formulas in which each clause contains at most two literals (\(2\mathsf{CNF}\)), and the class of circuits corresponding to Horn CNF formulas (\(\mathsf{HORN}\)). We formally state these results in the following corollary.

In what follows, we provide a proof of Theorem 7.

4.4 On the expressiveness of \(\mathrm{\small ExplAIner}\)↩︎

\(\mathrm{\small ExplAIner}\) allows us to express in a simple way the basic notions of explainability studied in this paper. Moreover, its evaluation problem is tractable given access to \(\mathrm{\small SAT}\) solvers. 4 shows how all the queries defined in Section 2.2 can be expressed in the \(\mathrm{\small ExplAIner}\) logic. Just for clarity we use unguarded universal quantifiers, which are not allowed according to the \(\mathrm{\small ExplAIner}\) syntax, because in these cases they can be rewritten as negations of unguarded existential quantifiers, as we discussed in Section 4.3. We also make use of some auxiliary predicates defined in the appendix (refer to Section 8.7).

Probably the most complicated formula of this section is the one used to express the query of relevant feature \(\mathsf{RF}(x, y)\). The idea there is to guess a weak abductive explanation \(w\) containing the assigned feature under consideration and verify that undefining the feature makes \(w\) lose the property of weak abductiveness. In fact, suppose first that \(y\) is indeed a relevant feature for \(x\). Then some abductive explanation \(w\) contains \(y\). Because \(w\) is minimal, undefining \(y\) from \(w\) cannot produce another weak abductive explanation, so the witness pair \(w, z\) exists. Conversely, if \(y\) is not a relevant feature for \(x\), then it cannot be contained in any minimal abductive explanation for \(x\). Assume toward a contradiction that there exist witnesses \(w\) and \(z\) for the formula, where \(w\) is a weak abductive explanation containing \(y\), \(z\) is obtained from \(w\) by undefining \(y\), and \(z\) is not a weak abductive explanation. Now let \(u \subseteq w\) be an abductive explanation. As \(y\) is not relevant, \(u\) cannot contain \(y\), and therefore \(u \subseteq z\). Since every completion of \(z\) is also a completion of \(u\), it would follow that \(z\) is a weak abductive explanation, a contradiction. Hence no such witness pair \(w, z\) can exist.

It should be noted that if \(\mathcal{C}\) is a class of models such that Eval\((\mathsf{AllPos}(x), \mathcal{C}) \in {\rm P}\) but Eval\((\mathsf{AllNeg}(x), \mathcal{C}) \not\in {\rm P}\) (under standard complexity-theoretic assumptions), then we still have that the problem Eval\((\psi, \mathcal{C})\) is in the Boolean hierarchy for the \(\mathrm{\small ExplAIner}\) formulas \(\psi\) that do not mention the predicate \(\mathsf{AllNeg}(x)\). Hence, the evaluation problem for this restricted fragment is still in the Boolean hierarchy, thus satisfying our criteria for an interpretability logic. This is the case, for example, for \(\mathsf{CNF}\) formulas, for which validity checks can be done in polynomial time but checking unsatisfiability is \({\rm coNP}\)-complete. In this case, we can still express queries such as minimum change required and maximum change allowed, since they can be expressed in \(\mathrm{\small ExplAIner}\) without mentioning the predicate \(\mathsf{AllNeg}(x)\). Similarly, if \(\mathcal{C}\) is a class of models such that Eval\((\mathsf{AllNeg}(x), \mathcal{C}) \in {\rm P}\) but Eval\((\mathsf{AllPos}(x), \mathcal{C}) \not\in {\rm P}\) (for example, \(\mathsf{DNF}\) formulas), then we still have that the evaluation problem is in the Boolean hierarchy for \(\mathrm{\small ExplAIner}\) formulas \(\psi\) that do not mention the predicate \(\mathsf{AllPos}(x)\).

Despite all the virtues of \(\mathrm{\small ExplAIner}\), unfortunately it is in general not able to solve computation problems efficiently. In fact, note that the ability to tractably evaluate queries over concrete partial instances does not directly imply that positive answers to the query can be constructed efficiently. We devote the rest of the paper to addressing this problem and propose a third logic that resolves it.

5 Opt-FOIL: computing explanations efficiently↩︎

Given an \(\mathrm{\small ExplAIner}\) formula \(\varphi(x, u_1, \ldots, u_k)\), we use the notation \(\varphi[u_1, \ldots, u_k](x)\) to indicate that \(x\) is a distinguished variable and \(u_1, \ldots, u_k\) are parameters that define the possible values for \(x\). In general, we use this syntax when \(x\) stores an explanation given an assignment for the variables \(u_1\), \(\ldots\), \(u_\ell\). For example, we write \(\varphi[u](x) = \mathsf{AXp}(u, x)\) to indicate that \(x\) is an abductive explanation given an assignment for the variable \(u\) (that is, \(x\) is an abductive explanation for \(u\)).

For each query \(\varphi[x_1, \ldots, x_k](x)\) in \(\mathrm{\small ExplAIner}\) and \(\mathcal{C}\) a class of models, we define the computation problem \(\mathsf{Comp}(\varphi, \mathcal{C})\) as follows:

5.1 The computational drawback of ExplAIner↩︎

We proved in Section 4.3 that the \(\mathrm{\small ExplAIner}\) logic admits tractable evaluations over adequate classes of models, which allows us to check if a partial instance is an answer for some explainability query. The next step in the study of \(\mathrm{\small ExplAIner}\) is to establish the complexity of actually computing such answers. Unfortunately, the following result tells us that this problem cannot be solved with a polynomial number of calls to an \({\rm NP}\) oracle, showing an important limitation of \(\mathrm{\small ExplAIner}\).

Proof. Consider the following ExplAIner formula: \[\varphi(x, y, z) \;:= \;{\sf MaxRel}(x, y) \wedge \neg \exists w \;[{\sf MaxRel}(w, z) \wedge x \subseteq w \wedge \mathsf{AllNeg}(w)],\] where \({\sf MaxRel}(x,y)\), defined during the proof of Theorem 2, is a formula from the atomic layer of ExplAIner such that \(\mathcal{M}\models {\sf MaxRel}(\mathbf{e},\mathbf{e}')\) if and only if \(\mathbf{e}_\bot = \mathbf{e}'_\bot\), i.e., the sets of undefined features in \(\mathbf{e}\) and \(\mathbf{e}'\) are the same. Now consider the formula \(\varphi(y, z) := \exists x\;\varphi(x, y, z)\), which is a FOIL formula with predicates \(\{\subseteq, \preceq, \mathsf{AllPos}, \mathsf{AllNeg}\}\). We will show that Eval\((\varphi, \mathsf{DTree})\) is \({\rm NP}^{{\rm NP}}\)-hard by a Karp reduction from the following well-known \({\rm NP}^{{\rm NP}}\)-complete problem (see [44] for a reference): given a propositional formula \(\alpha(\boldsymbol{p}, \boldsymbol{q})\) in \(\mathsf{DNF}\), where \(\boldsymbol{p}\) and \(\boldsymbol{q}\) are sets of variables, decide if the quantified propositional formula \(\exists \boldsymbol{p} \forall \boldsymbol{q}\;\alpha(\boldsymbol{p}, \boldsymbol{q})\) is true. We will describe a polynomial-time reduction that constructs a decision tree \(\mathcal{T}_{\alpha}\) and partial instances \(\mathbf{e}_{\alpha}, \mathbf{e}_{\alpha}'\) such that \(\exists \boldsymbol{p} \forall \boldsymbol{q}\;\alpha(\boldsymbol{p}, \boldsymbol{q})\) is true if and only if \(\mathcal{T}_{\alpha} \models \varphi(\mathbf{e}_{\alpha}, \mathbf{e}_{\alpha}')\).

Let \(n\) be the number of terms in \(\alpha\). We construct a decision tree \(\mathcal{T}_{\alpha}\) of dimension \(n + |\boldsymbol{p}| + |\boldsymbol{q}|\). We partition the features of \(\mathcal{T}_{\alpha}\) into three consecutive blocks \(H\), \(E\) and \(U\), where \(|H| = n\), \(|E| = |\boldsymbol{p}|\), and \(|U| = |\boldsymbol{q}|\). The block \(H\) will be used to select a term from \(\alpha\), while \(E\) and \(U\) will encode truth assignments to the existential \(\boldsymbol{p}\) and to the universal variables \(\boldsymbol{q}\), respectively.

For every term \(h_r\) (\(1 \leq r \leq n\)) we construct a decision tree \(C_r\) over \(E\) and \(U\) features in such a way that an input to that tree encoding a truth assignment reaches a \(\mathbf{true}\) leaf if and only if the term \(h_r\) evaluated over that assignment is \(\mathbf{true}\). We now explain how to construct \(\mathcal{T}_{\alpha}\). We use the feature corresponding to term \(h_{1}\) as the root. For every \(i < n\), the outgoing edge of \(h_i\) labeled by \(1\) is connected to \(h_{i+1}\), and the outgoing edge of \(h_n\) labeled by \(1\) is connected to a \(\mathbf{false}\) leaf. Also, for every \(i\), we connect the outgoing edge labeled by \(0\) of \(h_i\) to a copy of the tree \(C_i\). An example is shown in 5.

Set \(\mathbf{e}_{\alpha} = \{\bot\}^{n} \cdot \{0\}^{|\boldsymbol{p}|} \cdot \{\bot\}^{|\boldsymbol{q}|}\) and \(\mathbf{e}_{\alpha}' = \{\bot\}^{n} \cdot \{0\}^{|\boldsymbol{p}|+|\boldsymbol{q}|}\). We now show that the reduction is correct.

First suppose that \(\exists \boldsymbol{p} \forall \boldsymbol{q}\;\alpha(\boldsymbol{p}, \boldsymbol{q})\) is true. Let \(\nu\) be a truth assignment for the variables \(\boldsymbol{p}\) such that for every truth assignment \(\sigma\) for the variables \(\boldsymbol{q}\) it holds that \(\alpha(\nu(\boldsymbol{p}), \sigma(\boldsymbol{q}))\) is true. Let \(\mathbf{e}_{\alpha}''\) be a partial instance with just its \(E\) features defined according to \(\nu\). Notice that \(\mathbf{e}_{\alpha}''\) and \(\mathbf{e}_{\alpha}\) have the same defined features. We claim that \(\varphi(\mathbf{e}_{\alpha}'', \mathbf{e}_{\alpha}, \mathbf{e}_{\alpha}')\). In fact, let \(\mathbf{e}_{\alpha}'''\) be a partial instance with the same defined features as \(\mathbf{e}_{\alpha}'\) and such that \(\mathbf{e}_{\alpha}'' \subseteq \mathbf{e}_{\alpha}'''\). Notice that \(\mathbf{e}_{\alpha}'''\) naturally encodes a truth assignment \(\sigma\) for the variables \(\boldsymbol{q}\) together with \(\nu\). By taking a completion of \(\mathbf{e}_{\alpha}'''\) that has a \(0\) in the feature corresponding to a true term under the truth assignment \((\nu, \sigma)\) and a \(1\) in the features corresponding to all previous terms, we can see that \(\neg \mathsf{AllNeg}(\mathbf{e}_{\alpha}''')\). This shows that \(\varphi(\mathbf{e}_{\alpha}'', \mathbf{e}_{\alpha}, \mathbf{e}_{\alpha}')\), and therefore \(\mathcal{T}_{\alpha} \models \varphi(\mathbf{e}_{\alpha}, \mathbf{e}_{\alpha}')\).

Now suppose that \(\mathcal{T}_{\alpha} \models \varphi(\mathbf{e}_{\alpha}, \mathbf{e}_{\alpha}')\), so that there exists a partial instance \(\mathbf{e}_{\alpha}''\) such that \(\varphi(\mathbf{e}_{\alpha}'', \mathbf{e}_{\alpha}, \mathbf{e}_{\alpha}')\). Because \(\mathbf{e}_{\alpha}''\) has the same defined features as \(\mathbf{e}_{\alpha}\), we can define a truth assignment \(\nu\) for the variables \(\boldsymbol{p}\) according to \(\mathbf{e}_{\alpha}''\). Now let \(\sigma\) be any truth assignment for the variables \(\boldsymbol{q}\). We claim that \(\alpha(\nu(\boldsymbol{p}), \sigma(\boldsymbol{q}))\) is true. In fact, let \(\mathbf{e}_{\alpha}'''\) be the partial instance with the same defined features as \(\mathbf{e}_{\alpha}'\) and which corresponds to the pair \((\nu, \sigma)\). Because we have that \(\varphi(\mathbf{e}_{\alpha}'', \mathbf{e}_{\alpha}, \mathbf{e}_{\alpha}')\), it must be the case that \(\neg \mathsf{AllNeg}(\mathbf{e}_{\alpha}''')\). That means that there exists a completion of \(\mathbf{e}_{\alpha}'''\) that is evaluated as \(\mathbf{true}\) by \(\mathcal{T}_{\alpha}\). That necessarily means that there is a term in \(\alpha(\nu(\boldsymbol{p}), \sigma(\boldsymbol{q}))\) that is being satisfied. Hence \(\exists \boldsymbol{p} \forall \boldsymbol{q}\;\alpha(\boldsymbol{p}, \boldsymbol{q})\) is true.

This reduction shows that Eval\((\varphi, \mathsf{DTree})\) is \({\rm NP}^{{\rm NP}}\)-hard. To conclude the proof of the theorem, assume for the sake of contradiction that \(\mathsf{Comp}(\varphi[y, z](x),\, \mathsf{DTree}) \in {\rm FP}^{{\rm NP}}\). Then, it is clear that we would have Eval\((\varphi, \mathsf{DTree}) \in {\rm P}^{{\rm NP}}\). Finally, \({\rm P}^{{\rm NP}} = {\rm NP}^{{\rm NP}}\) implies that \({\rm PH}= {\rm P}^{{\rm NP}}\). ◻

To solve the problem that Theorem 8 signifies, we now propose \(\mathrm{\small Opt-FOIL}\), a logic that is defined by introducing a minimality operator over a subset of \(\mathrm{\small ExplAIner}\). As we will show in the next section, \(\mathrm{\small Opt-FOIL}\) meets all the criteria for an appropriate interpretability logic.

5.2 The Opt-FOIL logic↩︎

Our aim is to capture the right subset of \(\mathrm{\small ExplAIner}\) that meets all the criteria for an interpretability logic. For this, we will define a third logic called \(\mathrm{\small Opt-FOIL}\). We will show that the computation problem for this logic can be solved in polynomial time with a polynomial number of calls to an \({\rm NP}\) oracle.

We will say that a formula \(\rho(x, y, v_1, \ldots, v_\ell)\) from the atomic layer of \(\mathrm{\small ExplAIner}\) represents a strict partial order if, for every natural number \(n\) and assignment of partial instances of dimension \(n\) to the variables \(v_1\), \(\ldots\), \(v_\ell\), the resulting binary relation over the variables \(x\) and \(y\) is a strict partial order over the partial instances of dimension \(n\). Formally, \(\rho(x, y, v_1, \ldots, v_\ell)\) represents a strict partial order if, for every \(n \in \mathbb{N}\), \[\mathfrak{B}_n \models \;\forall v_1 \cdots \forall v_\ell \, \big[ \forall x \, \neg \rho(x, x, v_1, \ldots, v_\ell) \wedge \forall x \forall y \forall z \,\big( (\rho(x, y, v_1, \ldots, v_\ell) \wedge \rho(y, z, v_1, \ldots, v_\ell)) \to \rho(x, z, v_1, \ldots, v_\ell)\big)\big].\]

The variables \(v_1\), \(\ldots\), \(v_\ell\) in the formula \(\rho(x, y, v_1, \ldots, v_\ell)\) are considered as parameters that define a strict partial order. In fact, different assignments for these variables can give rise to different orders. Hence, we use the notation \(\rho[v_1, \ldots, v_\ell](x, y)\) to make explicit the distinction between the parameters \(v_1\), \(\ldots\), \(v_\ell\) and the variables \(x\), \(y\) that are instantiated with partial instances. For example, the strict partial order determined by the subsumption relation is defined by the formula \(\rho_1(x, y) = x \subset y\).

As a second example, consider the case where a certain feature must be disregarded when defining an order on partial instances (for instance, it is often undesirable to use the feature gender for comparisons). Such an order can be defined as follows. Notice that, with the appropriate values for the variables \(v_1\) and \(v_2\), the following formula checks whether the \(i\)-th feature of \(x\) is undefined: \[\mathsf{UF}(x, v_1, v_2) \;:= \;\neg(v_1 \subseteq x) \wedge \neg(v_2 \subseteq x).\] For example, if we are considering partial instances of dimension \(5\) and we need to check whether instance \(x\) has value \(\bot\) in the first feature, then we can use the values \(c_1 = (0, \bot, \bot, \bot, \bot)\) and \(c_2 = (1, \bot, \bot, \bot, \bot)\) for the variables \(v_1\) and \(v_2\), respectively. Moreover, let \[\mathsf{Pr}(x, y) \;:= \;x \subset y \wedge \neg \exists z \, (x \subset z \wedge z \subset y)\] be a formula that checks whether \(x\) is a predecessor of \(y\) under the order \(\subset\). Now define \[\mathsf{Strip}[v_1,v_2](x, y) \;:= \;(\mathsf{UF}(x,v_1,v_2) \wedge x=y) \;\vee \;(\neg \mathsf{UF}(x,v_1,v_2) \wedge \mathsf{Pr}(y,x) \wedge \mathsf{UF}(y,v_1,v_2)).\] Notice that, with the appropriate values for \(v_1\) and \(v_2\), \(\mathsf{Strip}[v_1,v_2](x,y)\) holds if and only if \(y\) is obtained from \(x\) by undefining the distinguished feature when necessary. Then, the following formula defines a strict partial order based on \(\subset\) but that disregards the \(i\)-th feature when comparing partial instances: \[\rho_2[v_1,v_2](x,y) \;:= \;\exists x' \exists y' \;\bigl(\mathsf{Strip}[v_1,v_2](x,x') \, \wedge \, \mathsf{Strip}[v_1,v_2](y,y') \, \wedge \, x' \subset y' \bigr).\]

For example, \(\rho_2[c_1, c_2](x, y)\) with constants \(c_1\) and \(c_2\) mentioned above defines a strict partial order that disregards the first feature when comparing partial instances of dimension \(5\).

Formulas from the atomic layer of \(\mathrm{\small ExplAIner}\) representing strict partial orders will be used in the definition of \(\mathrm{\small Opt-FOIL}\). Hence, it is necessary to have an algorithm that verifies whether this condition is satisfied in order to have a decidable syntax for \(\mathrm{\small Opt-FOIL}\). We will now prove that such an algorithm exists.

Proposition 9 serves as a theoretical upper bound to prove that \(\mathrm{\small Opt-FOIL}\) has a decidable syntax. Observe that if we restrict ourselves to formulas of bounded width, then the space complexity falls from triple exponential to double exponential in \(|\rho|\) (which implies that the time complexity is triple exponential in \(|\rho|\)). In practice, we expect formulas representing strict partial orders to be small and to have a simple structure, so we do not expect this theoretical high computational complexity to pose an actual implementation obstacle.

We now explain how strict partial orders will be used in the logic \(\mathrm{\small Opt-FOIL}\).

Given a formula \(\varphi[u_1, \ldots, u_k](x)\) from the quantified layer of ExplAIner and another formula \(\rho[v_1, \ldots, v_\ell](y, z)\) from the atomic layer of ExplAIner that represents a strict partial order, an \(\mathrm{\small Opt-FOIL}\) formula is an expression of the following form: \[\Psi[u_1, \ldots, u_k, v_1, \ldots, v_\ell](x) \;= \;\text{\rm min}[\varphi[u_1, \ldots, u_k](x), \rho[v_1, \ldots, v_\ell](y, z)].\]

Notice that \(x\), \(u_1, \ldots, u_k\), \(v_1, \ldots, v_\ell\) are the free variables of this expression, while the variables \(y\), \(z\) will be quantified. In particular, \(u_1, \ldots, u_k\) are the parameters that define the notion of explanation, \(v_1, \ldots, v_\ell\) are the parameters that define the strict partial order, and \(x\) is a variable used to store an explanation that is minimal in the sense given by the strict partial order. The semantics of \(\Psi[u_1, \ldots, u_k, v_1, \ldots, v_\ell](x)\) is defined by considering the following ExplAIner formula: \[\theta_{\text{\rm min}}(x, u_1, \ldots, u_k, v_1, \ldots, v_\ell) \;:= \;\varphi(x, u_1, \ldots, u_k) \;\wedge \; \neg \exists y \;\big(\varphi(y, u_1, \ldots, u_k) \, \wedge \, \rho(y, x, v_1, \ldots, v_\ell)\big).\] More precisely, given a model \(\mathcal{M}\) of dimension \(n\) and partial instances \(\mathbf{e}\), \(\mathbf{e}'_1, \ldots, \mathbf{e}'_k\), \(\mathbf{e}''_1, \ldots, \mathbf{e}''_\ell\) of dimension \(n\), we define that \(\mathcal{M}\models \Psi[\mathbf{e}'_1, \ldots, \mathbf{e}'_k, \mathbf{e}''_1, \ldots, \mathbf{e}''_\ell](\mathbf{e})\) if and only if \(\mathcal{M}\models \theta_{\text{\rm min}}(\mathbf{e}, \mathbf{e}'_1, \ldots, \mathbf{e}'_k, \mathbf{e}''_1, \ldots, \mathbf{e}''_\ell)\).

The computation problem for \(\mathrm{\small Opt-FOIL}\) has to be defined considering the different roles of the variables in the formula \(\Psi[u_1, \ldots, u_k, v_1, \ldots, v_\ell](x)\). In particular, the parameters \(u_1, \ldots, u_k, v_1, \ldots, v_\ell\) should be given as input, while the value of \(x\) is the explanation to be computed. The following definition takes these considerations into account. As usual, we write \(\mathcal{C}\) to denote some class of models.

We now show that \(\mathrm{\small Opt-FOIL}\) fulfills our criteria by establishing that the computation problem for \(\mathrm{\small Opt-FOIL}\) can be solved in polynomial time with a polynomial number of calls to an \({\rm NP}\) oracle:

As a corollary of this result, we obtain that \(\mathrm{\small Opt-FOIL}\) can be used to compute explanations in polynomial time using a polynomial number of calls to an \({\rm NP}\) oracle for the class of decision trees. Moreover, the same holds for more expressive representation classes, including \(\mathsf{d}\text{-}\mathsf{DNNF}\) circuits and fragments of the class of circuits corresponding to propositional formulas in conjunctive normal form (\(\mathsf{CNF}\)) whose satisfiability is decidable in polynomial time, such as 2-CNF formulas (\(2\mathsf{CNF}\)) and Horn CNF formulas (\(\mathsf{HORN}\)). We formally state these results in the following corollary.

We now begin the study of the expressiveness of \(\mathrm{\small Opt-FOIL}\). As is customary, we say that a logic \(\mathcal{L}_1\) is contained in a logic \(\mathcal{L}_2\) if for every formula in \(\mathcal{L}_1\) there exists an equivalent formula in \(\mathcal{L}_2\). Moreover, \(\mathcal{L}_1\) is properly contained in \(\mathcal{L}_2\) if \(\mathcal{L}_1\) is contained in \(\mathcal{L}_2\) and \(\mathcal{L}_2\) is not contained in \(\mathcal{L}_1\). The following proposition shows that the expressive power of \(\mathrm{\small Opt-FOIL}\) is less than that of \(\mathrm{\small ExplAIner}\), which in turn has less expressive power than \(\mathrm{\small FOIL}\) with predicates \(\{\subseteq, \preceq, \mathsf{AllPos}, \mathsf{AllNeg}\}\).

The logic \(\mathrm{\small Opt-FOIL}\) allows us to express in a simple way all notions of explainability that we study in this paper. For example, recall from Section 4.2 that \(\mathsf{wAXp}(u,x)\) can be expressed as a formula from the quantified layer of ExplAIner. Therefore, taking \(\varphi[u](x) = \mathsf{wAXp}(u,x)\), the following \(\mathrm{\small Opt-FOIL}\) formulas encode the notions of minimal and minimum abductive explanations: \[\begin{align} \mathsf{AXp}[u](x) &=& \text{\rm min}[\varphi[u](x), y \subset z],\\ \mathsf{mAXp}[u](x) &=& \text{\rm min}[\varphi[u](x), y \prec z ]. \end{align}\] Likewise, \(\text{\rm min}[\varphi[u](x), \rho_2[v_1,v_2](y, z)]\) encodes the notion of abductive explanations for the order \(\rho_2[v_1,v_2](y, z)\) that disregards a feature. The different variants of contrastive explanations can be expressed similarly.

As a second example, consider the notion of minimum change required and the predicate \(\mathsf{LEH}\) defined in Section 8.7. Then, taking \[\varphi[u](x) = \mathsf{Full}(u) \wedge \mathsf{Full}(x) \wedge \neg (\mathsf{AllPos}(u) \leftrightarrow \mathsf{AllPos}(x))\] and \(\rho_3[u](y,z) = \mathsf{LEH}(u,y,z) \wedge \neg \mathsf{LEH}(u,z,y)\), we can express the notion of minimum change required in \(\mathrm{\small Opt-FOIL}\) as follows: \[\begin{align} \mathsf{MCR}[u](x) = \text{\rm min}[\varphi[u](x), \rho_3[u](y,z)]. \end{align}\] By reversing the order, the logic \(\mathrm{\small Opt-FOIL}\) can also be used to express notions of explainability that involve maximality conditions. For example, consider the query of maximum change allowed that asks for the maximum number of changes that can be made to an instance without changing the output of the classification model. Taking \[\varphi[u](x) = \mathsf{Full}(u) \wedge \mathsf{Full}(x) \wedge (\mathsf{AllPos}(u) \leftrightarrow \mathsf{AllPos}(x))\] and defining the reverse order \(\rho_4[u](y,z) = \rho_3[u](z,y)\), we can express the notion of maximum change allowed in \(\mathrm{\small Opt-FOIL}\) as follows: \[\begin{align} \mathsf{MCA}[u](x) = \text{\rm min}[\varphi[u](x), \rho_4[u](y,z)]. \end{align}\] An important advantage of \(\mathrm{\small Opt-FOIL}\) is that it allows for the combination of explainability notions. For example, given two instances \(u_1\) and \(u_2\) of the same dimension, consider the query \(\mathsf{CAXp}[u_1, u_2](x) = \mathsf{wAXp}(u_1,x) \wedge \mathsf{wAXp}(u_2,x)\) that checks whether \(x\) is a common weak abductive explanation for \(u_1\) and \(u_2\). Then the following \(\mathrm{\small Opt-FOIL}\) formula computes a common weak abductive explanation for two instances (if such an explanation exists): \[\begin{align} \Psi_1[u_1,u_2](x) = \text{\rm min}[\mathsf{CAXp}[u_1, u_2](x), y \subset z]. \end{align}\] Note that an answer to this query is not necessarily minimal with respect to all weak abductive explanations for either \(u_1\) or \(u_2\).

Finally, another advantage of \(\mathrm{\small Opt-FOIL}\) is that it allows for the exploration of the space of explanations for a given classification. For example, assume that we already have an abductive explanation \(u_1\) for an instance \(u\), which can be computed using the \(\mathrm{\small Opt-FOIL}\) formula \(\mathsf{AXp}[u](x)\). Our aim is to compute a second abductive explanation \(u_2\) for \(u\). Consider the formula: \[\begin{align} \mathsf{SAXp}[u,u_1](x) = \mathsf{wAXp}(u, x) \wedge \mathsf{wAXp}(u, u_1) \wedge \neg (u_1 \subseteq x). \end{align}\] This formula checks whether \(x\) is a weak abductive explanation for \(u\) that does not subsume the abductive explanation \(u_1\). Thus, an abductive explanation for the instance \(u\) that is different from \(u_1\) can be computed using the following \(\mathrm{\small Opt-FOIL}\) formula: \[\begin{align} \Psi_2[u,u_1](x) = \text{\rm min}[\mathsf{SAXp}[u, u_1](x), y \subset z]. \end{align}\] We can apply the same idea to other notions of explanation, such as the \(\mathsf{MCR}\) explainability query, in order to compute multiple explanations for the output of a classification model.

6 Concluding remarks and future work↩︎

We have proposed a declarative approach to model interpretability based on query languages for explaining Boolean classification models. The starting point of our work is the observation that the growing number of explanation notions studied in formal XAI calls for a uniform language in which such notions can be specified, combined, and analyzed. This view is natural from a data management perspective: explanation notions become queries, models become the structures over which these queries are evaluated, and the main questions are those of expressiveness, evaluation complexity, and computation of answers.

Our first contribution was to revisit \(\mathrm{\small FOIL}\) from this perspective. We showed that, despite its foundational role, \(\mathrm{\small FOIL}\) is not well suited as a practical query language for explanations. On the one hand, it cannot express some central optimality-based notions, such as minimum abductive explanations, even over decision trees. On the other hand, its evaluation problem over decision trees is hard for every level of the polynomial hierarchy. These results show that a useful explainability language must carefully balance expressive power with controlled evaluation complexity.

To address this challenge, we introduced ExplAIner, a layered query language with an extended vocabulary for reasoning about partial instances and the behavior of Boolean models. We showed that ExplAInercan express a broad family of explanation notions, including abductive, contrastive, feature-based, and distance-based queries. At the same time, we proved that the evaluation problem for each fixed ExplAInerquery belongs to the Boolean hierarchy over every class of Boolean models for which the predicates \(\mathsf{AllPos}\) and \(\mathsf{AllNeg}\) can be evaluated in polynomial time. This condition holds not only for decision trees, but also for more general representation classes such as deterministic and decomposable Boolean circuits.

We also introduced Opt-FOIL, an optimization-oriented fragment of ExplAInerfor computing explanations that are minimal with respect to strict partial orders. This fragment captures a wide range of optimality-based explanation tasks while retaining controlled computational behavior: under the same assumptions on \(\mathsf{AllPos}\) and \(\mathsf{AllNeg}\), explanations specified in Opt-FOILcan be computed in \(\mathrm{FP}^{\mathrm{NP}}\). Together, the results for ExplAInerand Opt-FOILshow that declarative specification and complexity-theoretic analysis can provide a principled foundation for model interpretability.

Several directions remain open. A first direction is to extend the framework beyond Boolean classification models. Although Boolean models are standard in formal XAI and already capture many explanation tasks, many applications involve multi-class outputs, non-Boolean features, or structured feature domains. It would be interesting to understand which parts of the present framework extend directly to these richer settings, and which additional predicates or language constructs are needed.

A second direction is to study further model representations. Our upper bounds are stated for every class of Boolean models over which \(\mathsf{AllPos}\) and \(\mathsf{AllNeg}\) can be evaluated in polynomial time, and this already includes decision trees and deterministic decomposable Boolean circuits. A natural next step is to identify additional representation classes that satisfy this condition. This would help clarify the connection between explainability languages and knowledge compilation more broadly.

A third direction concerns query optimization. One of the motivations for a declarative language is that different explanation notions can share common subqueries and operators. This suggests the possibility of developing optimization techniques for explainability queries, in the same spirit as query optimization in databases. Such techniques could exploit common subformulas, reuse calls to procedures for \(\mathsf{AllPos}\) and \(\mathsf{AllNeg}\), or identify fragments with better evaluation strategies.

Finally, it would be valuable to study richer answer mechanisms for explainability queries. In this paper, explanations are treated as partial instances satisfying a logical specification, possibly optimized with respect to a strict partial order. However, users may require different levels of detail, multiple alternative explanations, or rankings of explanations according to several criteria. Extending the language with principled mechanisms for enumeration, ranking, and comparison of explanations is an important step toward a more complete declarative framework for model interpretability.

7 Acknowledgements↩︎

Part of this work has been funded by ANID - Millennium Science Initiative Program - Code ICN17002. Diego Bustamante was partially funded by ANID - Subdirección de Capital Humano (Magíster Nacional, 2023, folio 22231282). María Alejandra Schild was financially supported by ANID (Doctorado Nacional, 2025, folio 21251617). Bernardo Subercaseaux is (partially) supported by the DARPA expMath program through the DARPA CMO contract number HR0011262E028.

8 Supplementary Material↩︎

8.1 Proof of Lemma 1↩︎

We will first prove an auxiliary result. We start by introducing some terminology.

Let \(U = \{a_i \mid i > 0\}\) be a countably infinite set. We take a disjoint copy \(\overline{U} = \{\overline{a}_i \mid i > 0\}\) of \(U\). For an \(X \subseteq U \cup \overline{U}\), we define \[\begin{align} X_{U \setminus \overline{U}} \;& := \;\{a \in U \mid a \in X \text{ and } \overline{a} \not\in X\} \\ X_{U \cap \overline{U}} \;& := \;\{a \in U \mid a \in X \text{ and } \overline{a} \in X\} \\ X_{\overline{U} \setminus U} \;& := \;\{\overline{a} \in \overline{U} \mid \overline{a} \in X \text{ and } a \not\in X\} \end{align}\] The \(\ell\)-type of \(X\), for \(\ell \geq 0\), is the tuple \[\big(\min{\{\ell,|X_{U \setminus \overline{U}}|\}},\, \min{\{\ell,|X_{U \cap \overline{U}}|\}}, \, \min{\{\ell,|X_{\overline{U} \setminus U}|\}}\big).\] We write \(X \leftrightarrows_\ell X'\), for \(X,X' \subseteq U \cup \overline{U}\), if \(X\) and \(X'\) have the same \(\ell\)-type. If \(X \subseteq U \cup \overline{U}\), then \(X\) is well formed (wf) if for each \(i > 0\) at most one element from \(\{a_i,\overline{a}_i\}\) is in \(X\).

We now consider structures of the form \(\mathfrak{A}^* = \langle 2^{X},\subseteq^{\mathfrak{A}^*} \rangle\), where \(X \subseteq U \cup \overline{U}\) and \(\subseteq^{\mathfrak{A}^*}\) is the relation that contains all pairs \((Y,Z)\), for \(Y,Z \subseteq X\), such that \(Y \subseteq Z\). Given two structures \(\mathfrak{A}^*_1\) and \(\mathfrak{A}^*_2\) of this form, perhaps with constants, we write \(\mathfrak{A}^*_1 \equiv_k^{{\rm wf}} \mathfrak{A}^*_2\) to denote that the Duplicator has a winning strategy in the \(k\)-round Ehrenfeucht-Fraı̈ssé game played on structures \(\mathfrak{A}^*_1\) and \(\mathfrak{A}^*_2\), but where Spoiler and Duplicator are forced to play wf subsets of \(U \cup \overline{U}\) only.

Consider structures \(\mathfrak{A}^*_1 = \langle 2^{X_1},\subseteq^{\mathfrak{A}^*_1} \rangle\) and \(\mathfrak{A}^*_2 = \langle 2^{X_2},\subseteq^{\mathfrak{A}^*_2} \rangle\) of the form described above. We claim that, for every \(k \geq 0\),

\[\label{eq:wf} X_1 \leftrightarrows_{3^k} X_2 \quad \Longrightarrow \quad \big(\mathfrak{A}^*_1,(X_1 \cap U)\big) \;\equiv_k^{{\rm wf}} \; \big(\mathfrak{A}^*_2,(X_2 \cap U)\big).\tag{5}\]

Before proving the claim 5 , we explain how it implies Lemma 1. Take a structure of the form \({\mathfrak{A}_n = \langle \{0,1,\bot\}^n,\subseteq^{\mathfrak{A}_n}\rangle}\), where \(\subseteq^{\mathfrak{A}_n}\) is the subsumption relation over \(\{0,1,\bot\}^n\). Take, on the other hand, the structure \(\mathfrak{A}_n^* = \langle 2^X,\subseteq^{\mathfrak{A}_n^*} \rangle\), where \(X = \{a_1,\dots,a_n,\bar a_1,\dots,\bar a_n\}\). It can be seen that there is an isomorphism \(f\) between \(\mathfrak{A}_n\) and the substructure of \(\mathfrak{A}_n^*\) induced by the wf subsets of \(X\). The isomorphism \(f\) takes an instance \(\mathbf{e}\in \{0,1,\bot\}^n\) and maps it to \(Y \subseteq X\) such that for every \(i \in \{1,\dots,n\}\), (a) if \(\mathbf{e}[i] = 1\) then \(a_i \in Y\), (b) if \(\mathbf{e}[i] = 0\) then \(\bar a_i \in Y\), and (c) if \(\mathbf{e}[i] = \bot\) then neither \(a_i\) nor \(\bar a_i\) is in \(Y\). By definition, the isomorphism \(f\) maps the tuple \(\{1\}^n\) in \(\mathfrak{A}_n\) to the set \(X \cap U = \{a_1,\dots,a_n\}\) in \(\mathfrak{A}^*_n\).

From claim 5 , it follows then that if \(n,p \geq 3^k\) it is the case that \[(\mathfrak{A}^*_n,\{a_1,\dots,a_n\}) \;\equiv_k^{{\rm wf}} \; (\mathfrak{A}^*_p,\{a_1,\dots,a_p\}).\] From our previous observations, this implies that \[(\mathfrak{A}_n,\{1\}^n) \;\equiv_k \; (\mathfrak{A}_p,\{1\}^p).\] We conclude, in particular, that \(\mathfrak{A}^+_n \equiv_k \mathfrak{A}^+_p\), as desired.

We now prove the claim in 5 . We do it by induction on \(k \geq 0\). The base cases \(k = 0\) and \(k= 1\) are immediate. We now move to the induction case for \(k+1\). Take structures \(\mathfrak{A}^*_1 = \langle 2^{X_1},\subseteq^{\mathfrak{A}^*_1} \rangle\) and \(\mathfrak{A}^*_2 = \langle 2^{X_2},\subseteq^{\mathfrak{A}^*_2} \rangle\) of the form described above, such that \(X_1 \leftrightarrows_{3^{k+1}} X_2\). Assume, without loss of generality, that for the first round the Spoiler picks the well formed element \(X'_1 \subseteq X_1\) in the structure \(\mathfrak{A}^*_1\). From Lemma 7, there exists \(X'_2 \subseteq X_2\) such that \[X'_1 \leftrightarrows_{3^k} X'_2 \;\;\text{ and } \;\;X_1\setminus X'_1 \leftrightarrows_{3^k} X_2 \setminus X'_2.\] By induction hypothesis, the following holds: \[\begin{align} \big(\langle 2^{X'_1},\subseteq \rangle,(X'_1 \cap U)\big) & \equiv^{\rm wf}_k & \big(\langle 2^{X'_2},\subseteq \rangle,(X'_2 \cap U)\big)\\ \big(\langle 2^{X_1 \setminus X'_1},\subseteq \rangle,((X_1 \setminus X'_1) \cap U)\big) & \equiv^{\rm wf}_k & \big(\langle 2^{X_2 \setminus X'_2},\subseteq \rangle,((X_2 \setminus X'_2) \cap U)\big). \end{align}\] A simple composition argument allows to obtain the following from these two expressions: \[\label{eq:final} \big(\langle 2^{X_1},\subseteq \rangle,(X_1 \cap U),X'_1\big) \;\equiv_k^{{\rm wf}} \;\big(\langle 2^{X_2},\subseteq \rangle, (X_2 \cap U),X'_2\big).\tag{6}\] This holds because \(X'_1 = (X_1 \cap U)\) iff \(X'_2 = (X_2 \cap U)\). In fact, assume that \(X'_1 = (X_1 \cap U)\), so that \(X'_1 \cap \overline{U} = \emptyset\). Since \(X'_1 \leftrightarrows_{3^k} X'_2\), it follows that \(X'_2 \subseteq X_2 \cap U\). On the other hand, \(X_1 \setminus X_1' = X_1 \cap \overline{U}\). As \(X_1 \setminus X_1' \leftrightarrows_{3^k} X_2 \setminus X'_2\), we conclude that \(X_2 \setminus X'_2 \subseteq \overline{U}\), and hence \(X_2 \cap U \subseteq X_2'\). Combining both inclusions, we obtain that \(X'_2 = (X_2 \cap U)\). The other direction is completely analogous.

But Equation 6 is equivalent with the following fact: \[\big(\langle 2^{X_1},\subseteq \rangle,(X_1 \cap U)\big) \;\equiv_{k+1}^{{\rm wf}} \;\big(\langle 2^{X_2},\subseteq \rangle, (X_2 \cap U) \big).\] This finishes the proof of Lemma 1.

8.2 Proof of Lemma 2↩︎

Let \(\mathbf{e}_i\) and \(\mathbf{e}'_i\) be the moves played by Spoiler and Duplicator in \(\mathfrak{A}_\mathcal{M}\oplus \mathfrak{A}_{\mathcal{M}_1}\) and \(\mathfrak{A}_\mathcal{M}\oplus \mathfrak{A}_{\mathcal{M}_2}\), respectively, for the first \(i \leq k\) rounds of the Ehrenfeucht-Fraı̈ssé game \[\begin{align} \big(\mathfrak{A}_\mathcal{M}\oplus \mathfrak{A}_{\mathcal{M}_1},\{1\}^{n+p},\{\bot\}^n \cdot \{1\}^p\big) \;\equiv_k \; \big(\mathfrak{A}_\mathcal{M}\oplus \mathfrak{A}_{\mathcal{M}_2},\{1\}^{n+q},\{\bot\}^n \cdot \{1\}^q\big). \end{align}\] We write \(\mathbf{e}_i = (\mathbf{e}_{i1},\mathbf{e}_{i2})\) to denote that \(\mathbf{e}_{i1}\) is the tuple formed by the first \(n\) features of \(\mathbf{e}_i\) and \(\mathbf{e}_{i2}\) is the one formed by the last \(p\) features of \(\mathbf{e}_i\). Similarly, we write \(\mathbf{e}'_i = (\mathbf{e}'_{i1},\mathbf{e}'_{i2})\) to denote that \(\mathbf{e}'_{i1}\) is the tuple formed by the first \(n\) features of \(\mathbf{e}'_i\) and \(\mathbf{e}'_{i2}\) is the one formed by the last \(q\) features of \(\mathbf{e}'_i\).

The winning strategy for Duplicator is as follows. Suppose \(i-1\) rounds have been played, and for round \(i\) the Spoiler picks element \(\mathbf{e}_i \in \mathfrak{A}_\mathcal{M}\oplus \mathfrak{A}_{\mathcal{M}_1}\) (the case when he picks an element in \(\mathfrak{A}_\mathcal{M}\oplus \mathfrak{A}_{\mathcal{M}_2}\) is symmetric). Assume also that \(\mathbf{e}_i = (\mathbf{e}_{i1},\mathbf{e}_{i2})\). The duplicator then considers the position \[\big((\mathbf{e}_{12},\dots,\mathbf{e}_{(i-1)2}),(\mathbf{e}'_{12},\dots,\mathbf{e}'_{(i-1)2})\big)\] on the game \((\mathfrak{A}_{\mathcal{M}_1},\{1\}^p) \equiv_k (\mathfrak{A}_{\mathcal{M}_2},\{1\}^q)\), and finds his response \(\mathbf{e}'_{i2}\) to \(\mathbf{e}_{i2}\) in \(\mathfrak{A}_{\mathcal{M}_2}\). The Duplicator then responds to the Spoiler’s move \(\mathbf{e}_i \in \mathfrak{A}_\mathcal{M}\oplus \mathfrak{A}_{\mathcal{M}_1}\) by choosing the element \(\mathbf{e}'_i = (\mathbf{e}_{i1},\mathbf{e}'_{i2}) \in \mathfrak{A}_\mathcal{M}\oplus \mathfrak{A}_{\mathcal{M}_2}\).

Notice, by definition, that \(\mathbf{e}_i = \{1\}^{n+p}\) iff \(\mathbf{e}'_i = \{1\}^{n+q}\). Similarly, \(\mathbf{e}_i = \{\bot\}^n \cdot \{1\}^{p}\) iff \(\mathbf{e}'_i = \{\bot\}^n \cdot \{1\}^{q}\). Moreover, it is easy to see that playing in this way the Duplicator preserves the subsumption relation. Analogously, the strategy preserves the \(\mathsf{Pos}\) relation. In fact, \(\mathbf{e}_i\) is a positive instance of \(\mathfrak{A}_\mathcal{M}\oplus \mathfrak{A}_{\mathcal{M}_1}\) iff \(\mathbf{e}_{i1}\) is a positive instance of \(\mathfrak{A}_\mathcal{M}\) or \(\mathbf{e}_{i2}\) is a positive instance of \(\mathfrak{A}_{\mathcal{M}_1}\). By definition, the latter follows if and only if \(\mathbf{e}_{i1}\) is a positive instance of \(\mathfrak{A}_\mathcal{M}\) or \(\mathbf{e}'_{i2}\) is a positive instance of \(\mathfrak{A}_{\mathcal{M}_2}\), which in turn is equivalent to \(\mathbf{e}'_i\) being a positive instance of \(\mathfrak{A}_\mathcal{M}\oplus \mathfrak{A}_{\mathcal{M}_2}\).

We conclude that this is a winning strategy for the Duplicator, and hence that \[\begin{align} \big(\mathfrak{A}_\mathcal{M}\oplus \mathfrak{A}_{\mathcal{M}_1},\{1\}^{n+p},\{\bot\}^n \cdot \{1\}^p\big) \;\equiv_k \; \big(\mathfrak{A}_\mathcal{M}\oplus \mathfrak{A}_{\mathcal{M}_2},\{1\}^{n+q},\{\bot\}^n \cdot \{1\}^q\big). \end{align}\] This finishes the proof of Lemma 2.

8.3 Proof of Lemma 3↩︎

To prove that \(\Sigma_{k+1}\)-QBF\((\mathsf{DTree})\) is in \(\Sigma_{k}^{\text{P}}\), note that we can decide in polynomial time if a given decision tree encodes a tautology. Therefore, we can use a \(\Sigma_k\)-alternating Turing machine for guessing the values for the first \(k\) quantifiers, we prune the decision tree according to those guesses, and then we solve the remaining universal quantifier directly.

For the hardness, we use a reduction from the following standard \(\Sigma_k^{\text{P}}\)-hard problem (see [45] for a reference): Given a 3CNF formula \(\varphi\) over the set \(X = \{x_1,\dots,x_m\}\) of propositional variables, is it the case that the expression \(\psi = \exists X_1 \forall X_2 \cdots \exists X_k \, \varphi\) holds, where \(X_1,\dots,X_k\) is a partition of \(X\) in \(k\) equivalence classes? Note that the hypothesis of \(k\) being odd is important here because if the last quantifier were universal, we could solve it directly as in the case of decision trees. From \(\psi\) we build in polynomial time a \(\Sigma_{k+1}\)-QBF \(\alpha\) over \(\mathcal{M}_\varphi\), where \(\mathcal{M}_\varphi\) is a decision tree that can be built in polynomial time from \(\varphi\), such that \[\label{eq:holds} \text{\psi holds} \quad \Longleftrightarrow \quad \text{\alpha holds.}\tag{7}\]

We now explain how to define \(\mathcal{M}_\varphi\) from the CNF formula \(\varphi\). Let \(\varphi = C_1 \wedge \cdots \wedge C_n\) be a propositional formula, where each \(C_i\) is a disjunction of three literals and does not contain repeated or complementary literals. Moreover, assume that \(\{x_1, \ldots, x_m\}\) is the set of variables occurring in \(\varphi\), and the proof will use partial instances of dimension \(n+m\). Notice that the last \(m\) features of such a partial instance \(\mathbf{e}\) naturally define a truth assignment for the propositional formula \(\varphi\). More precisely, for every \(i \in \{1, \ldots, n\}\), we use notation \(\mathbf{e}(C_i) = 1\) to indicate that there is a disjunct \(\ell\) of \(C_i\) such that \(\ell = x_j\) and \(\mathbf{e}[n+j] = 1\), or \(\ell = \neg x_j\) and \(\mathbf{e}[n+j] = 0\), for some \(j \in \{1,\ldots,m\}\). Furthermore, we write \(\mathbf{e}(\varphi) = 1\) if \(\mathbf{e}(C_i) = 1\) for every \(i \in \{1, \ldots, n\}\).

For each clause \(C_i\) (\(i \in \{1, \ldots, n\}\)), let \(\mathcal{M}_{C_i}\) be a decision tree of dimension \(n+m\) (but that will only use features \(n+1, \ldots, n+m\)) such that for every instance \(\mathbf{e}\): \(\mathcal{M}_{C_i}(\mathbf{e}) = 1\) if and only if \(\mathbf{e}(C_i) = 1\). Notice that \(\mathcal{M}_{C_i}\) can be constructed in constant time as it only needs to contain at most eight paths of depth 3. For example, assuming that \(C = (x_1 \vee x_2 \vee x_3)\), a possible decision tree \(\mathcal{M}_C\) is depicted in the following figure:

Moreover, define \(\mathcal{M}_\varphi\) as the following decision tree.

Recall that the set of features of \(\mathcal{M}_\varphi\) is \([1,n+m]\). The formula \(\alpha\) is defined as \[\exists P_1 \forall P_2 \cdots \exists P_k \forall P \, \mathcal{M}_\varphi,\] assuming that \(P_i\), for \(1 \leq i \leq k\), is the set \(\{n+\ell \mid x_\ell \in X_i\}\), and \(P = \{1,\dots,n\}\). That is, \(P_i\) is the set of features from \(\mathcal{M}_\varphi\) that represent the variables in \(X_i\) and \(P\) is the set of features that are used to encode the clauses of \(\varphi\).

We show next that the equivalence stated in 7 holds. For simplicity, we only do it for the case \(k = 1\). The proof for \(k > 1\) uses exactly the same ideas, only that it is slightly more cumbersome.

Assume, on the one hand, that \(\psi = \exists X_1 \varphi\) holds. That is, there exists an assignment \(\sigma_1 : X_1 \to \{0,1\}\) such that \(\varphi\) holds when variables in \(X_1\) are interpreted according to \(\sigma_1\). We show next that \(\alpha = \exists P_1 \forall P \mathcal{M}_\varphi\) holds, where \(P_1\) and \(P\) are defined as above. Take the partial instance \(\mathbf{e}_{\sigma_1}\) of dimension \(n + m\) that naturally “represents” the assignment \(\sigma_1\); that is:

• \(\mathbf{e}_{\sigma_1}[i] = \bot\), for each \(i \in \{1,\dots,n\}\),

• \(\mathbf{e}_{\sigma_1}[n+i] = \sigma_1(x_i)\), for each \(i \in \{1,\dots,m\}\) with \(x_i \in X_1\), and

• \(\mathbf{e}_{\sigma_1}[n+i] = \bot\), for each \(i \in \{1,\dots,m\}\) with \(x_i \not\in X_1\).

To show that \(\alpha\) holds, it suffices to show that \(\mathcal{M}_\varphi(\mathbf{e}) = 1\) for every instance \(\mathbf{e}\) of dimension \(n+m\) that subsumes \(\mathbf{e}_{\sigma_1}\). Take an arbitrary such an instance \(\mathbf{e}\in \{0,1\}^{n+m}\). Notice that if \(\mathbf{e}[i] = 1\), for every \(i \in \{1,\dots,n\}\), then \(\mathcal{M}_\varphi(\mathbf{e}) = 1\) by definition of \(\mathcal{M}_\varphi\). Suppose then that there exists a minimum value \(i \in \{1,\dots,n\}\) such that \(\mathbf{e}[i] = 0\). Hence, to show that \(\mathcal{M}_\varphi(\mathbf{e}) = 1\) we need to show that \(\mathcal{M}_{C_i}(\mathbf{e}) = 1\). But this follows easily from the fact that \(\mathbf{e}\) naturally represents an assignment \(\sigma\) for \(\varphi\) such that the restriction of \(\sigma\) to \(X_1\) is precisely \(\sigma_1\). We know that any such an assignment \(\sigma\) satisfies \(\varphi\), and therefore it satisfies \(C_i\). It follows that \(\mathcal{M}_{C_i}(\mathbf{e}) = 1\).

Assume, on the other hand, that \(\alpha = \exists P_1 \forall P \mathcal{M}_\varphi\) holds. Then there exists a partial instance \(\mathbf{e}\) of dimension \(n+m\) such that the following statements hold:

• \(\mathbf{e}[i] \neq \bot\) iff for some \(j \in \{1,\dots,m\}\) it is the case that \(i = n + j\) and \(j \in P_1\), and

• for every \(\mathbf{e}' \in \textit{comp}(\mathbf{e})\) we have that \(\mathcal{M}_\varphi(\mathbf{e}') = 1\).

We show next that \(\psi = \exists X_1 \varphi\) holds. Let \(\sigma_1 : X_1 \to \{0,1\}\) be the assignment for the variables in \(X_1\) that is naturally defined by \(\mathbf{e}\). It suffices to show that each clause \(C_i\) of \(\varphi\), for \(i \in \{1,\dots,n\}\), is satisfied by the assignment that interprets the variables in \(X_1\) according to \(\sigma_1\). Let us define a completion \(\mathbf{e}'\) of \(\mathbf{e}\) that satisfies the following:

• \(\mathbf{e}'[i] = 0\),

• \(\mathbf{e}'[j] = 1\), for each \(j \in \{1,\dots,n\}\) with \(i \neq j\), and

• \(\mathbf{e}'[n+j] = \sigma_1(x_j)\), if \(j \in \{1,\dots,m\}\) and \(j \in P_1\).

We know that \(\mathcal{M}_\varphi(\mathbf{e}') = 1\), which implies that \(\mathcal{M}_{C_i}(\mathbf{e}') = 1\) (since \(\mathbf{e}'\) takes value 0 for feature \(i\)). We conclude that \(C_i\) is satisfied by the assignment which is naturally defined by \(\mathbf{e}'\), which is precisely the one that interprets the variables in \(X_1\) according to \(\sigma_1\).

8.4 Proof of Lemma 4↩︎

We induct on the depth of \(\varphi\). First we will see the atomic cases:

• For atomic formulas of the form \(x_i = x_j\), we take \[\sum_{\substack{\rho \in \{0, 1, \bot \}^k \\ \rho_i \neq \rho_j}}{z_\rho} \; = \; 0.\]

• For atomic formulas of the form \(x_i \subseteq x_j\), we take \[\sum_{\substack{\rho \in \{0, 1, \bot \}^k \\ \rho_i \neq \rho_j \; \land \; \rho_i \neq \bot}}{z_\rho} \; = \; 0.\]

• For atomic formulas of the form \(x_i \preceq x_j\), we take \[\sum_{\substack{\rho \in \{0, 1, \bot \}^k \\ \rho_j = \bot}}{z_\rho} \; \leq \; \sum_{\substack{\rho \in \{0, 1, \bot \}^k \\ \rho_i = \bot}}{z_\rho}.\]

Now we describe the structural induction. For the negation, it is enough to take \(\operatorname{T}_\Gamma(\neg \psi)\bigl((z_\rho)_\rho\bigr)\) as \(\neg \operatorname{T}_\Gamma(\psi)\bigl((z_\rho)_\rho\bigr)\). If \(\varphi\) is of the form \(\psi_1 \circ \psi_2\), where \(\circ\) is a binary logical connective, then we take \(\operatorname{T}_\Gamma(\varphi)\bigl((z_\rho)_\rho\bigr)\) as \[\operatorname{T}_\Gamma(\psi_1)\bigl((z_\rho)\bigr) \; \circ \; \operatorname{T}_\Gamma(\psi_2)\bigl((z_\rho)\bigr).\] Note that here it is important to use the inductive hypothesis with \(\Gamma\) that contains both the free variables of \(\psi_1\) and of \(\psi_2\). We need to be more careful if \(\varphi\) is of the form \(\exists u\, \psi(y_1, \dots, y_\ell, u)\). By changing the name of the variable if necessary, we can assume that \(u \not \in \Gamma\). Consider \(\Lambda = (x_1, \dots, x_k, u)\) and take the formula \[\operatorname{T}_\Lambda(\psi)\bigl((w_\tau)_{\tau\in\{0,1,\bot\}^{k+1}}\bigr)\] given by the inductive hypothesis. We take \(\operatorname{T}_\Gamma(\varphi)\bigl((z_\rho)_{\rho\in\{0,1,\bot\}^{k}}\bigr)\) to be \[\exists (w_\tau)_{\tau\in\{0,1,\bot\}^{k+1}} \quad \operatorname{Proj}_{\Lambda \to \Gamma}((w_\tau)_\tau,\, (z_\rho)_\rho) \; \land \; \operatorname{T}_\Lambda(\psi)\bigl((w_\tau)_{\tau\in\{0,1,\bot\}^{k+1}}\bigr),\] where \(\operatorname{Proj}_{\Lambda \to \Gamma}((w_\tau)_\tau,\, (z_\rho)_\rho)\) is defined to be \[\bigwedge_{\rho\in\{0,1,\bot\}^{k}}{z_{\rho} = w_{(\rho, 0)} + w_{(\rho, 1)} + w_{(\rho, \bot)}}.\] Finally, if \(\varphi\) is of the form \(\forall u\, \psi(y_1, \dots, y_\ell, u)\), we define \(\Lambda\) as before and take \(\operatorname{T}_\Gamma(\varphi)\bigl((z_\rho)_{\rho\in\{0,1,\bot\}^{k}}\bigr)\) to be \[\forall (w_\tau)_{\tau\in\{0,1,\bot\}^{k+1}} \quad \bigl(\operatorname{Proj}_{\Lambda \to \Gamma}((w_\tau)_\tau,\, (z_\rho)_\rho) \; \rightarrow \; \operatorname{T}_\Lambda(\psi)\bigl((w_\tau)_{\tau\in\{0,1,\bot\}^{k+1}}\bigr) \bigr).\] For the second part of the lemma, note that for a subformula translated in a context \(\Gamma\) of size \(k\), the corresponding Presburger formula has \(3^k\) variables. In the atomic cases we just need to manage sums without repetitions over those variables. Boolean connectives also do not cause any problems. In the case of quantifiers, we need to increase the size of the context from \(k\) to \(k+1\) and we also add \(3^k\) projection formulas plus the recursive call. But because \(k+1 \leq \rm{wd}(\varphi)\) and there are \(O(|\varphi|)\) subformulas, the total output size is \(O(|\varphi| \cdot 3^{\rm{wd}(\varphi)})\) up to polynomial factors of \(\rm{wd}(\varphi)\). Notice that the same argument applies for proving that the computation itself can be done using at most that same space.

8.5 Proof of Lemma 5↩︎

Consider the following similar problem. The input is a model \(\mathcal{M}'\), an instance \(\mathbf{e}'\) and a \(k \in \mathbb{N}\), and the question is whether there exists a partial instance \(\mathbf{e}\) that is a weak abductive explanation for \(\mathbf{e}'\) on \(\mathcal{M}'\) and whose number of defined features is at most \(k\). This problem was studied in [21], where it was shown to be \({\rm NP}\)-hard on decision trees. We show a reduction from this problem.

First assume that \(\mathcal{M}'(\mathbf{e}') = 1\). We create new variables \(X_{i}\) for \(i\in \{0,1,...,k\}\). Let \(\mathcal{M}\) be a new decision tree such that \(\dim(\mathcal{M}) = k + 1 + \dim(\mathcal{M}')\), depicted in the following figure:

We use \(X_{0}\) as the root of \(\mathcal{M}\). For every \(i < k\), the outgoing edge of \(X_i\) labeled by \(1\) is connected to \(X_{i+1}\), and the outgoing edge of \(X_k\) labeled by \(1\) is connected to a \(\mathbf{true}\) leaf. Connect all outgoing edges labeled by \(0\) to a copy of \(\mathcal{M}'\). Let \(\mathbf{e}_1 = \{1\}^{k+1} \cdot \mathbf{e}'\) and \(\mathbf{e}_2 = \{1\}^{k+1} \cdot \{\bot\}^{\dim(\mathcal{M}')}\) be partial instances of size \({\textit dim}(\mathcal{M})\). We claim that \(\mathbf{e}_2\) is a minimum abductive explanation for \(\mathbf{e}_1\) on \(\mathcal{M}\) if and only if the answer to the original problem was negative. For the case \(\mathcal{M}'(\mathbf{e}') = 0\) we can just set the value of the new leaf to \(\mathbf{false}\) and the same construction will work.

We now discuss why the reduction works. Suppose first that \((\mathcal{M}', \mathbf{e}', k)\) outputs \(\mathrm{\small Yes}\). It follows that there exists a partial instance \(\mathbf{e}\) on \(\mathcal{M}'\) that is a weak abductive explanation for \(\mathbf{e}'\) with at most \(k\) defined features. Now notice that the partial instance \(\{\bot\}^{k+1} \cdot \mathbf{e}\) is a weak abductive explanation for \(\mathbf{e}_1\) on \(\mathcal{M}\) and has at most \(k\) defined features. Because \(\mathbf{e}_2\) has \(k+1\) defined features, it follows that \(\mathbf{e}_2\) is not a minimum abductive explanation for \(\mathbf{e}_1\) on \(\mathcal{M}\).

Now suppose that \((\mathcal{M}', \mathbf{e}', k)\) outputs \(\mathrm{\small No}\). Then there is no weak abductive explanation for \(\mathbf{e}'\) on \(\mathcal{M}'\) with at most \(k\) defined features. This implies that there is also no partial instance \(\mathbf{e}\) on \(\mathcal{M}\) that is a weak abductive explanation for \(\mathbf{e}_1\) with at most \(k\) defined features. This is because any candidate weak abductive explanation for \(\mathbf{e}_1\) with at most \(k\) defined features leaves at least one of the new variables undefined, and therefore some completion of it reaches a copy of \(\mathcal{M}'\). Once it enters that copy of \(\mathcal{M}'\), its restrictions on the old coordinates would induce a weak abductive explanation for \(\mathbf{e}'\) on \(\mathcal{M}'\) with at most \(k\) defined features, contradicting the assumption. But we know that \(\mathbf{e}_2\) is a weak abductive explanation for \(\mathbf{e}_1\) with \(k+1\) defined features, so it is a minimum abductive explanation for \(\mathbf{e}_1\) on \(\mathcal{M}\), as we needed.

8.6 Proof of Lemma 6↩︎

We first treat the parameter-free case \(\rho(x,y)\), and then we extend the idea to the general case.

Fix a dimension \(n\). Given a partial instance of dimension \(n\), define \(\#_0(\mathbf{e})\) as the number of occurrences of the symbol \(0\) in \(\mathbf{e}\), and likewise for \(\#_1(\mathbf{e})\) and \(\#_\bot(\mathbf{e})\). Moreover, for every \((p,q,r) \in \mathbb{N}^3\) such that \(p + q + r = n\), define \[\begin{align} L_{(p,q,r)} \;:= \;\{ \mathbf{e}\mid \mathbf{e}\text{ is a partial instance of dimension } n \text{ such that } \#_0(\mathbf{e}) = p,\, \#_1(\mathbf{e}) = q \text{ and } \#_\bot(\mathbf{e}) = r \}. \end{align}\] Notice that there are at most \(\binom{n+2}{2} \leq (n+1)^2\) different sets \(L_{(p,q,r)}\). We claim that if \(\mathbf{e}_1\) and \(\mathbf{e}_2\) are partial instances of dimension \(n\) such that \(\mathbf{e}_1, \mathbf{e}_2 \in L_{(p,q,r)}\) for the same triple \((p, q, r)\), then \(\mathfrak{B}_n \not\models \rho(\mathbf{e}_1, \mathbf{e}_2)\). From that we can conclude that the statement of the lemma holds for \(p(n) = (n+1)^2\), since if \((\mathbf{e}_1, \ldots, \mathbf{e}_k)\) is a path of dimension \(n\) in \(\rho(x,y)\), then each \(\mathbf{e}_i\) must belong to a different set \(L_{(p,q,r)}\).

For the sake of contradiction, suppose that \(\mathbf{e}_1, \mathbf{e}_2\) are two different partial instances of dimension \(n\) that belong to the same set \(L_{(p, q, r)}\) and such that \(\mathfrak{B}_n \models \rho(\mathbf{e}_1, \mathbf{e}_2)\). Then there exists a permutation \(\pi : \{1, \ldots, n\} \to \{1, \ldots, n\}\) such that \(\pi(\mathbf{e}_1) = \mathbf{e}_2\). Notice that for every pair \(\mathbf{e}\), \(\mathbf{e}'\) of partial instances of dimension \(n\) it holds that: \[\begin{align} \mathbf{e}\subseteq \mathbf{e}' &\quad\quad\Leftrightarrow\quad\quad \pi(\mathbf{e}) \subseteq \pi(\mathbf{e}')\\ \mathbf{e}\preceq\mathbf{e}' &\quad\quad\Leftrightarrow\quad\quad \pi(\mathbf{e}) \preceq\pi(\mathbf{e}'). \end{align}\] Thus, \(\pi\) is an automorphism for the structure \(\mathfrak{B}_n\). Because we have that \(\mathfrak{B}_n \models \rho(\mathbf{e}_1, \mathbf{e}_2)\), and \(\rho\) is defined over the vocabulary \(\{ \subseteq, \preceq\}\), it follows \(\mathfrak{B}_n \models \rho(\pi(\mathbf{e}_1), \pi(\mathbf{e}_2))\). But since \(\mathbf{e}_2 = \pi(\mathbf{e}_1)\), we also have that \(\mathfrak{B}_n \models \rho(\mathbf{e}_2, \pi(\pi(\mathbf{e}_1)))\). Because \(\rho(x, y)\) is transitive, it follows that \(\mathfrak{B}_n \models \rho(\mathbf{e}_1, \pi^2(\mathbf{e}_1))\). In the same way, we can conclude that \(\mathfrak{B}_n \models \rho(\mathbf{e}_1, \pi^k(\mathbf{e}_1))\) for every \(k \geq 1\). Given that the set of permutations of \(n\) elements with the composition operator forms a group of order \(n!\), we know that \(\pi^{n!}\) is the identity permutation, so that \(\pi^{n!}(\mathbf{e}_1) = \mathbf{e}_1\). Therefore, we conclude that \(\mathfrak{B}_n \models \rho(\mathbf{e}_1, \mathbf{e}_1)\), which leads to a contradiction since \(\rho(x,y)\) represents a strict partial order.

Consider now a formula \(\rho[v_1, \ldots, v_\ell](x,y)\) with parameters. As in the previous case, we fix a dimension \(n\). Moreover, we also fix a sequence \(\mathbf{e}'_1\), \(\ldots\), \(\mathbf{e}'_\ell\) of partial instances of dimension \(n\) (notice that the bound \(p(n)\) should not depend on those partial instances). Then, for every \((a_1, \ldots, a_\ell) \in \{0,1,\bot\}^\ell\), consider the set \[\begin{align} P_{(a_1, \ldots, a_\ell)} \;= \;\{i \in \{1, \ldots, n\} \;\mid \;\mathbf{e}'_j[i] = a_j \text{ for all } j \in \{1, \ldots, \ell\}\}, \end{align}\] that is, all positions for which the sequence \(\mathbf{e}'_1\), \(\ldots\), \(\mathbf{e}'_\ell\) realizes the pattern \((a_1, \ldots, a_\ell)\). Given \(s \in \{0, 1, \bot\}\), a pattern \(t \in \{0,1,\bot\}^\ell\) and a partial instance \(\mathbf{e}\) of dimension \(n\), define \(\#_{s, t}(\mathbf{e})\) as the number of indices \(i \in P_t\) such that \(\mathbf{e}[i]=s\). Notice that the numbers \(\#_{s, t}(\mathbf{e})\) are invariant under permutations of the features that map each pattern block onto itself.

We define an equivalence relation as follows. For two partial instances \(\mathbf{e}_1\) and \(\mathbf{e}_2\) of dimension \(n\), we write \(\mathbf{e}_1 \sim \mathbf{e}_2\) if \(\#_{s, t}(\mathbf{e}_1) = \#_{s, t}(\mathbf{e}_2)\) for every \(s \in \{0, 1, \bot\}\) and every \(t \in \{0,1,\bot\}^\ell\). Notice that there are at most \[\binom{n+3^{\ell+1}-1}{3^{\ell+1}-1} \leq \frac{\big(n+3^{\ell+1}-1\big)^{3^{\ell+1}-1}}{\big(3^{\ell+1}-1 \big)!}\] different equivalence classes. Because \(\ell\) is fixed, we can consider that number as our polynomial \(p(n)\).

We claim that if \(\mathbf{e}_1 \sim \mathbf{e}_2\), then \(\mathfrak{B}_n \not\models \rho[\mathbf{e}'_1, \ldots, \mathbf{e}'_\ell](\mathbf{e}_1, \mathbf{e}_2)\). From that we can conclude, as in the parameter-free case, that the statement of the lemma holds. In fact, if \((\mathbf{e}_1, \ldots, \mathbf{e}_k)\) is a path of dimension \(n\) in \(\rho[v_1, \ldots, v_\ell](x,y)\), then each \(\mathbf{e}_i\) must belong to a different equivalence class.

For the sake of contradiction, suppose that \(\mathbf{e}_1, \mathbf{e}_2\) are two different partial instances of dimension \(n\) such that \(\mathbf{e}_1 \sim \mathbf{e}_2\) and \(\mathfrak{B}_n \models \rho[\mathbf{e}'_1, \ldots, \mathbf{e}'_\ell](\mathbf{e}_1, \mathbf{e}_2)\). For each pattern block \(P_t\), consider a permutation \(\pi_t\) of \(P_t\) sending the restriction of \(\mathbf{e}_1\) on \(P_t\) to the restriction of \(\mathbf{e}_2\) on \(P_t\). Combining these permutations yields a permutation \(\pi : \{1, \ldots, n\} \to \{1, \ldots, n\}\) such that \(\pi(\mathbf{e}_1) = \mathbf{e}_2\). Notice that by the way we constructed the permutations \(\pi_t\) and the pattern blocks \(P_{t}\), we have that \(\pi(\mathbf{e}'_j) = \mathbf{e}'_j\) for every \(j \in \{1, \ldots, \ell\}\).

As in the parameter-free case, we have that \(\pi\) is an automorphism for the structure \(\mathfrak{B}_n\). Since \(\rho\) is a formula defined over the vocabulary \(\{\subseteq, \preceq\}\), and \(\mathfrak{B}_n \models \rho[\mathbf{e}'_1, \ldots, \mathbf{e}'_\ell](\mathbf{e}_1, \mathbf{e}_2)\), it follows that \(\mathfrak{B}_n \models \rho[\pi(\mathbf{e}'_1), \ldots, \pi(\mathbf{e}'_\ell)](\pi(\mathbf{e}_1), \pi(\mathbf{e}_2))\). Because \(\pi(\mathbf{e}'_j) = \mathbf{e}'_j\) for every \(j \in \{1, \ldots, \ell\}\) and \(\mathbf{e}_2 = \pi(\mathbf{e}_1)\), we obtain that \(\mathfrak{B}_n \models \rho[\mathbf{e}'_1, \ldots, \mathbf{e}'_\ell](\mathbf{e}_2, \pi(\pi(\mathbf{e}_1)))\), and using that \(\rho[\mathbf{e}'_1, \ldots, \mathbf{e}'_\ell](x, y)\) is transitive, we also have that \(\mathfrak{B}_n \models \rho[\mathbf{e}'_1, \ldots, \mathbf{e}'_\ell](\mathbf{e}_1, \pi^2(\mathbf{e}_1))\). In the same way, it is possible to conclude that \(\mathfrak{B}_n \models \rho[\mathbf{e}'_1, \ldots, \mathbf{e}'_\ell](\mathbf{e}_1, \pi^k(\mathbf{e}_1))\) for every \(k \geq 1\). Given that the set of permutations of \(n\) elements with the composition operator forms a group of order \(n!\), we know that \(\pi^{n!}\) is the identity permutation, so that \(\pi^{n!}(\mathbf{e}_1) = \mathbf{e}_1\). Therefore, we conclude that \(\mathfrak{B}_n \models \rho[\mathbf{e}'_1, \ldots, \mathbf{e}'_\ell](\mathbf{e}_1, \mathbf{e}_1)\), which leads to a contradiction since \(\rho[v_1, \ldots, v_\ell](x,y)\) represents a strict partial order.

8.7 Auxiliary predicates↩︎

8.7.0.1 Definition of the formula \(\mathsf{LEH}(x,y,z)\).

Let \(\mathsf{GLB}\) (Greatest Lower Bound) be the following formula: \[\begin{align} \mathsf{GLB}(x,y,z) \;:= \;z \subseteq x \wedge z \subseteq y \wedge \forall w \, ((w \subseteq x \wedge w \subseteq y) \to w \subseteq z). \end{align}\] The interpretation of this predicate is such that for every model \(\mathcal{M}\) of dimension \(n\) and every sequence of instances \(\mathbf{e}_1, \mathbf{e}_2, \mathbf{e}_3\) it holds that \(\mathcal{M}\models \mathsf{GLB}(\mathbf{e}_1, \mathbf{e}_2, \mathbf{e}_3)\) if and only if \(\mathbf{e}_3\) is the greatest partial instance subsumed by \(\mathbf{e}_1\) and \(\mathbf{e}_2\), i.e., the partial instance with most defined features subsumed by both. This property allows us to measure the number of defined features on which the two instances agree. By using this predicate, let \(\mathsf{LEH}\) be a ternary predicate such that \(\mathcal{M}\models \mathsf{LEH}(\mathbf{e}_1, \mathbf{e}_2, \mathbf{e}_3)\) if and only if the Hamming distance between \(\mathbf{e}_1\) and \(\mathbf{e}_2\) is less than or equal to the Hamming distance between \(\mathbf{e}_1\) and \(\mathbf{e}_3\). The relation \(\mathsf{LEH}\) can be expressed as a formula from the atomic layer of \(\mathrm{\small ExplAIner}\) as follows: \[\begin{align} \mathsf{LEH}(x,y,z) \;:= \;\mathsf{Full}(x) \wedge \mathsf{Full}(y) \wedge \mathsf{Full}(z) \;\wedge \exists w_1 \exists w_2 \, (\mathsf{GLB}(x,y,w_1) \wedge \mathsf{GLB}(x,z,w_2) \wedge w_2 \preceq w_1). \end{align}\]

8.7.0.2 Definition of the formula \(\mathsf{Add}(x,y,z)\).

Let \(\mathsf{LU}\) (Level Up) be the following formula: \[\begin{align} \mathsf{LU}(x, y) \;:= \;x \prec y \wedge \neg \exists z \;(x \prec z \wedge z \prec y), \end{align}\] such that \(\mathcal{M}\vDash \mathsf{LU}(\mathbf{e}_1, \mathbf{e}_2)\) if and only if \(\mathbf{e}_1\) has exactly one less defined feature than \(\mathbf{e}_2\). By using this predicate, let \(\mathsf{Add}\) be a ternary predicate such that \(\mathcal{M}\vDash \mathsf{Add}(\mathbf{e}_1, \mathbf{e}_2, \mathbf{e}_3)\) if and only if \(\mathbf{e}_2\) is a feature subsumed by \(\mathbf{e}_3\) and \(\mathbf{e}_1\) is obtained from \(\mathbf{e}_3\) by undefining the feature \(\mathbf{e}_2\). The relation \(\mathsf{Add}\) can be expressed as formula from the atomic layer of \(\mathrm{\small ExplAIner}\) as follows: \[\begin{align} \mathsf{Add}(x,y,z) \;:= \;{\sf Single}(y) \wedge x \subseteq z \wedge \mathsf{LU}(x, z) \wedge y \subseteq z \wedge \neg(y \subseteq x). \end{align}\] Recall that \({\sf Single}(x)\) defines the set of partial instances with exactly one defined feature, and can be expressed as follows: \[{\sf Single}(x) := \exists y (y \subset x) \wedge \forall y (y \subset x \, \rightarrow \, \neg \exists z (z \subset y)).\]

References↩︎