# Inherent Inconsistencies of Feature Importance

Nimrod Harel
Department of Computer Science
Tel-Aviv University
Tel Aviv, Israel
<EMAIL_ADDRESS>
Ran Gilad-Bachrach
Department of Biomedical Engineering
Tel-Aviv University
Tel Aviv, Israel
<EMAIL_ADDRESS>
Uri Obolski
School of Public Health
Porter School of the Environment and Earth Sciences
Tel-Aviv University
Tel Aviv, Israel
<EMAIL_ADDRESS>
###### Abstract

The black-box nature of modern machine learning techniques invokes a practical
and ethical need for explainability. Feature importance aims to meet this need
by assigning scores to features, so humans can understand their influence on
predictions. Feature importance can be used to explain predictions under
different settings: of the entire sample space or a specific instance; of
model behavior, or the dependencies in the data themselves. However, in most
cases thus far, each of these settings was studied in isolation.

We attempt to develop a sound feature importance score framework by defining a
small set of desired properties. Surprisingly, we prove an inconsistency
theorem, showing that the expected properties cannot hold simultaneously. To
overcome this difficulty, we propose the novel notion of re-partitioning the
feature space into separable sets. Such sets are constructed to contain
features that exhibit inter-set independence with respect to the target
variable. We show that there exists a unique maximal partitioning into
separable sets. Moreover, assigning scores to separable sets, instead of
single features, unifies the results of commonly used feature importance
scores and annihilates the inconsistencies we demonstrated.

##  1 Introduction

Many feature importance scores are inspired by, or derived from, Shapley’s
work on fair allocation in coalition games (1). In these, and other common
methods, the importance score is computed in a two-step process. First, a
value-function is computed, assigning a value to every subset of the features.
Different metrics can be used to define the value-function, such as mutual
information, classification accuracy, or the coefficient of determination.
Second, the importance score is computed of the values assigned to these
subsets. This two step process allows for a discussion about the expected
behavior of the value-function and of the feature importance score in relation
to the value-function. Here, we focus on several such feature importance
scores: ablation-studies (2; 3; 4), bivariate-association (5), SHAP (6) and
MCI (7). The definitions of these feature importance functions can be found in
Table 1.

The study of feature importance can be divided into four different settings,
across two axes: local and global, as well as data and model. Studies focusing
on local interpretations seek to explain individual predictions (e.g., the
role of each feature in a patient’s diagnosis (8)). On the other hand, studies
focusing on global interpretation try to understand how each feature affects a
phenomenon (e.g. the role of each gene in a particular disease (9; 10)). Along
the second axis, the data and the model are distinguished by the type of
conclusion required. The scientist seeks an explanation of the data, to infer
conclusions about the world that are encoded in the data (11; 12; 13). The
engineer, however, uses an explanation to monitor and debug a man-made system,
to ensure it is working as intended, e.g. for security purposes (14; 15).
Table 2 maps feature importance research according to the local vs. global and
data vs. model settings.

Several studies have examined the relations between the different settings.
For example, Lundberg et al. (16) presented a global score that is computed by
combining local scores, hence indicating that at least the local and the
global settings are not independent. Nevertheless, most studies focus solely
on one setting. The studies that do consider multiple settings, often do not
present an explicit set of expectations from the relations between importance
scores under the different settings.

In this work, we define the expected behaviors of feature importance scores
under different settings, and the expected relations between the settings. In
Section 2 we define, using formal language, the value-function, the feature
importance function, and the expected properties of these functions. For
example, the _Triviality_ property (Definition 2.3) requires that if the value
of a set of features is non-zero, then it contains a feature with non-zero
importance. We also add consistency requirements between the settings. The
_Importance Consistency_ property (Definition 2.2) requires that the global
importance score is the expected value of the local importance scores. The
_Data-Model Equivalence_ property (Definition 2.5) requires that a model that
perfectly predicts the entire sample space will generate the same feature
importance scores as those calculated on the data.

Naturally, the next step in our inquiry is to seek feature importance scores
that satisfy the required properties and are consistent between the settings.
However, in Section 3 we show that it is impossible to define such importance
scores. That is, properties of feature importance scores within and between
setting contradict each other. Hence, there are inherent inconsistencies
between the expected behaviors of feature importance scores in the different
settings.

Table 1: Examples of common feature importance functions | Name
---
| Feature importance score: $\boldsymbol{\phi(\nu,f)}$
---
| Bivariate
---
| $\nu(\\{f)\\}$
---
| Ablation
---
| $\nu(\mathcal{F})-\nu(\mathcal{F}\setminus\\{f\\})$
---
| Shapley
---
|
$\sum_{\mathcal{S}\subseteq\mathcal{F}\setminus\\{f\\}}\frac{|\mathcal{S}|!(|\mathcal{F}|-|\mathcal{S}|-1)!}{|\mathcal{F}|!}\cdot(\nu(\mathcal{S}\cup\\{f\\})-\nu(\mathcal{S}))$
---
| MCI
---
|
$\max_{\mathcal{S}\subseteq\mathcal{F}\setminus\\{f\\}}(\nu(\mathcal{S}\cup\\{f\\})-\nu(\mathcal{S}))$
---

We further exemplify practical gaps in feature importance scores when applied
to specific dependency structures. We show that the presence of highly
correlated features and collider variables yield inconsistent and misleading
interpretations of feature importance. Therefore, the use of feature
importance to study phenomena in the world might be deceiving even in the
presence of unlimited data and perfect models.

The inconsistencies of feature importance scores and their misleading behavior
jeopardize their use as valid explanations (17). In an attempt to find a
remedy for these inherent inconsistencies, we propose that scores can be
assigned to sets of features that are inter-set independent with respect to
the target variable. We term these _separable sets_ and prove that there
exists a unique maximal partition of the feature space into separable sets. We
consider these separable sets as “meta-features” and extend the feature
importance scores to them. We show that the commonly used importance scores
mentioned above consolidate when applied on separable sets. Finally, scores
applied to separable sets do not suffer from the inconsistencies of scores
assigned to individual features.

###  1.1 Related Work

Many feature importance scores have been proposed in the literature. Table 2
lists several popular feature importance scores and their mapping to the
different settings, according to the global-local and data-model divisions.
Most feature importance scores thus far focused on explaining models, although
the data setting has also been gaining increased attention in recent years.
However, the quadrant of the data-local setting is still unexplored in the
field of explainable AI. Perhaps this is due to the challenge of providing an
accurate explanation as to why a specific outcome (rather than average result)
came into being (rather than was calculated by a model). For example, which
characteristic of John Doe is responsible for the fact that he did, or did
not, suffer a stroke? These types of questions pertain to individual causal
effects, that are notoriously difficult to estimate (18; 19).

There is an ongoing discussion regarding the formulations and interpretations
of feature importance scores. Several studies attempted to link the scores
under different settings. Covert et al. (5) proposed a method of assigning
global importance to features, which draws a connection with the local feature
importance score of _SHAP_ (6). Chen et al. (20) defined distinctions between
the data and the model and argued that the nature of an explanation depends on
what one seeks to explain – the data or the model. Furthermore, despite their
popularity, the interpretation of Shapely value based methods has been
questioned by recent studies. Shapley based values can be invalid under co-
linearity between features (21; 22; 7), or when interpreting modification of
features as an intervention (23). These discussions motivate our attempt to
define expected properties of importance scores, which will allow us to gauge
the suitability of different solutions.

###  1.2 Our Contribution

The contributions of this work are:

  1. 1.

We propose a unified framework for the desired properties of different
settings of feature importance: global-data, local-data, global-model, and
local-model.

  2. 2.

We present intrinsic problems of inconsistency in feature importance scores
across the various settings:

     * •

We show that the requirement that global feature importance is the expected
value of local feature importance is inconsistent with results in the data
setting.

     * •

We show that results in the data setting and results in the model setting are
inconsistent, even in the case where the data and the model agree everywhere.

     * •

We show concrete examples in which feature importance scores fail to provide
the explanation we would have expected.

  3. 3.

Based on our results, we define a method of calculating importance scores for
sets of features that are inter-set independent with respect to the target
variable. We show that there exists a unique maximal partition to such
independent (separable) sets. This partition overcomes the aforementioned
difficulties and unifies the results of different feature importance score.
Therefore, we propose considering these separable sets as “meta-features” and
assigning scores to them.

The paper is structured as follows: The second section contains notations and
framework properties. The third section contains the inconsistency theorems
for the two axes we have presented earlier, as well as examples of internal
causal problems that appear in the feature importance method. The fourth
section contains our proposal for the limited case in which consistency is
maintained, as well as overcoming the problems we have presented.

Table 2: Examples of feature importance scores and their categorization according to the global/local and data/model settings |  Global |  Local
---|---|---
| Model
---
Additive-Importance-Measures (5) Bivariate-Association (5) Ablation-Studies (2; 3; 4) FIRM (24) Tree-Shap (16) |  SHAP (6) Lime (25) Gradient-Based-Localization (26) Relevance-Propagation (27) TreeExplainer (16)
| Data
---
True-To-Data (20) MCI (7) UMFI (28) |

##  2 Framework

###  2.1 Notation

We begin by introducing some notation: $x$ is an instance from the sample
space $\mathcal{X}$ and $y$ is a corresponding target variable from the target
space $\mathcal{Y}$ ; $f$ is a feature from the feature set $\mathcal{F}$; the
value-function $\nu$ assigns a real-valued score to every
$\mathcal{S}\subseteq\mathcal{F}$; the feature importance function $\phi$
assigns a real valued score to every feature $f\in\mathcal{F}$, based on the
value-function $\nu$. We use the modifiers $l/\mathbf{g}$ to distinguish
between the local/global settings, and the modifiers $\mathcal{M}/\mathcal{D}$
to distinguish between the model/data settings. For the sake of brevity, we
will omit the modifiers when their meaning is evident from the context, or
when a statement holds for all settings. When explicitly referring to a model
$\mathcal{M}$, $\mathcal{M}(x)$ will denote its prediction. Additionally,
$\phi(\nu,f)$ will denote the feature importance of $f$, whereas $\phi(\nu)$
will denote the vector of feature importance values for all the features at
hand. Finally, $\mathbb{E}$ will denote the expected value-function with
respect to the underlying distribution of $x\sim\mathcal{X}$.

A value-function is a function $\nu:2^{|\mathcal{F}|}\rightarrow\mathbb{R}$
that assigns a scalar to each subset of features
$\mathcal{S}\subseteq\mathcal{F}$, where $\nu(\mathcal{S})$ denotes the value
of a subset of features $\mathcal{S}$ . A feature importance function is a
function
$\phi:\mathbb{R}^{2^{|\mathcal{F}|}}\rightarrow\mathbb{R}^{|\mathcal{F}|}$
that receives the output of a value-function, and assigns a feature importance
score to each feature. We denote $\phi_{l}(\nu_{x})$ as the local feature
importance of instance $x$, and $\phi_{\mathbf{g}}(\nu_{\mathbf{g}})$ as the
global feature importance of the entire sample space $\mathcal{X}$.

###  2.2 Properties of feature importance under the different settings

In this section, we lay the foundations for the unified framework of feature
importance. We formulate requirements and properties that we expect to hold
for the value-function, the importance function and the relationships between
them under the different settings.

######  Definition 2.1 (Value Consistency)

$\nu$ is local-global consistent if $\forall\mathcal{S}\subseteq\mathcal{F}$,
it holds that

$\mathbb{E}[\nu_{x}(\mathcal{S})]=\nu_{\mathbf{g}}(S)$

To establish the local-global relation, we constrain the global value of each
subset (calculated by the global value-function) to be the expectancy of the
local value on this subset (calculated by the local value-function).

######  Definition 2.2 (Importance Consistency)

$\phi$ is local-global consistent if $\forall f\in\mathcal{F}$, it holds that

$\mathbb{E}[\phi_{l}(\nu_{x},f)]=\phi_{g}(\nu_{\mathbf{g}},f)$

To establish the local-global relations of the importance score, a similar
consistency requirement is made for the feature importance function: the
global importance of a feature (calculated by the global feature importance
function) is the expected value of the local feature importance of this
feature (calculated by the local feature importance function).

######  Definition 2.3 (Triviality)

The triviality requirement holds if

  1. 1.

$\forall\mathcal{S}\subseteq\mathcal{F}$, if $\nu(\mathcal{S})\neq 0$ then
$\exists f\in\mathcal{S}$ s.t $\phi(\nu,f)\neq 0$

  2. 2.

If $\phi(\nu,f)\neq 0$ then $\exists\mathcal{S}\subseteq\mathcal{F}$ s.t
$\nu(\mathcal{S}\cup\\{f\\})\neq\nu(\mathcal{S})$

The triviality requirement establishes a non-trivial relationship between the
value and the importance functions. Simply said, it requires that if a subset
of features has any value, it will be expressed in the importance of at least
one feature from this subset. In the other direction, it requires that if any
feature is important (i.e has non-zero importance) so this feature must be
included in some valuable subset. Note that it also holds that if a feature
$f$ is such that for any subset of features, $\nu(S)=\nu(S\cup\\{f\\})$ then
$f$ has zero importance.

######  Definition 2.4 (Null Feature)

If for $f\subseteq\mathcal{F},\forall x,x^{\prime}\in\mathcal{X}$, s.t $x$
differs from $x^{\prime}$ only at the $f$’th feature,
it holds that $\mathcal{M}(x)=\mathcal{M}(x^{\prime})$, then

$\phi(\nu^{\mathcal{M}},f)=0$

The null feature property states that if changing the value of a feature has
no effect on a model, then its importance is zero.

######  Definition 2.5 (Data-Model Equivalence)

$\phi$ is data-model consistent, if $\forall\mathcal{M},\mathcal{D}$ s.t
$\forall(x,y)\in(\mathcal{X},\mathcal{Y}),\mathcal{M}(x)=y$ it holds that
$\forall f\in\mathcal{F}$,

$\phi(\nu^{\mathcal{M}},f)=\phi(\nu^{\mathcal{D}},f)$

The data-model equivalence property states that if a model predicts the target
perfectly, then the data and model importance scores of each feature will be
identical.

Definitions 2.1 and 2.2 define the expected relation between explanations of
single case and explanations of the model or the data. Therefore, when they
both hold, we say that $(\phi,\nu)$ is local-global consistent. The later
definitions, namely Definitions 2.4 and 2.5, focus on the relation between
explaining the data and explaining a model. Therefore, when these three
definitions hold, we say that $(\phi,\nu)$ is data-model consistent.

The goal of stating these definition is to find consistent families of feature
importance scores. However, in the next section we show that such families do
not exist.

##  3 Feature importance inconsistencies

###  3.1 The local-global inconsistency

We begin by studying the local-global consistency in the data setting. In
addition to Definitions 2.1 and 2.2 we assume a set of properties, defined in
Catav et al. (7), that a feature importance score in the data-global setting
is expected to have. The properties described therein are the _Marginal
Contribution_ property, which states that
$\phi_{\mathbf{g}}(\nu,f)\geq\nu(\mathcal{F})-\nu(\mathcal{F}\setminus\\{f\\})$;
the _Elimination_ property, which states that if
$f\in\mathcal{F}\subseteq\mathcal{F}^{\prime}$, then the importance of $f$ in
the context of $\mathcal{F}^{\prime}$ is not smaller then its importance in
the context of $\mathcal{F}$; and the _Minimalism_ property, which requires
that a feature importance score is the minimal score function that satisfies
the _Marginal Contribution_ and _Elimination_ properties. Formal definitions
of the properties are attached in the Supplementary Material.

###### Theorem 1

The assumptions of the data-global setting (the Marginal Contribution
property, the Elimination property, and the Minimalism property) cannot hold
simultaneously with the local-global consistency of $(\phi,\nu)$ (Definitions
2.1,2.2).

The proof uses the following two lemmas, which proofs are attached in the
Supplementary Material.

###### Lemma 1

If $(\nu,\phi)$ is local-global consistent, then $\forall x\in\mathcal{X}$, it
holds that

$\phi_{\mathbf{g}}(\nu_{x})=\phi_{l}(\nu_{x})$

Note that we did not require the feature importance function to be identical
in the local and global case. The lemma states that under these assumptions,
the global and local feature importance functions are identical.

###### Lemma 2

If $(\nu,\phi)$ is local-global consistent, then $\phi_{\mathbf{g}}$ is a
linear function of $\nu_{\mathbf{g}}$.

Proof. [of Theorem 1]

Assume in contradiction that $(\nu,\phi)$ is local-global consistent in the
data setting. From Lemma 1 it holds that $\phi_{\mathbf{g}}\equiv\phi_{l}$,
and from Lemma 2 we have the $\phi_{\mathbf{g}}$ is a linear function.
However, Catav et al. (7) proved that the only function that satisfies the
_Marginal Contribution_ property, the _Elimination_ property, and the
_Minimalism_ property is MCI which is not a linear function. $\Box$

A numeric example showing that MCI is not linear can be found in the
Supplementary Material.

###  3.2 The data-model inconsistency

Models are often used as a proxy to represent the world. In cases where the
model is perfect, i.e., the model predictions are identical to the data, we
would expect the data and the model to also agree on each feature’s
importance. However, this expectation implies a degenerate case, where the
value-function is the zero function.

###### Theorem 2

If Triviality holds and $(\nu,\phi)$ is data-model consistent (Definitions
2.3,2.4, 2.5), then $\nu\equiv 0$.

Proof.  Let $\rho$ be a random variable, and let $f_{0},f_{1}$ be two features
s.t $f_{0}=f_{1}=\rho$. Let $(\nu,\phi)$ be data-model consistent, and let
$\mathcal{M}^{0},\mathcal{M}^{1}$ be two models s.t each model focuses on one
feature and neglects the other: for $i=\\{0,1\\}$,
$\mathcal{M}^{i}(x)=f_{i}(x)$.

Assume in contradiction that $\forall
i\in\\{0,1\\},\nu^{\mathcal{M}^{i}}\not\equiv 0$.
$\mathcal{M}^{0},\mathcal{M}^{1}$ are identical to the data$~{}\rho$, and
therefore $\forall
f\in\mathcal{F},\phi(\nu^{\mathcal{M}^{i}},f)=\phi(\nu^{\mathcal{D}},f)$ by
the _Data-Model Equivalence_ property.

By the _Null Feature_ property, we get that
$\phi(\nu^{\mathcal{M}^{i}},f_{1-i})=0$. We assumed that the value-function is
not the zero function, hence by _Triviality_ it holds that
$\exists\mathcal{S}\subseteq\mathcal{F}$ s.t
$\nu^{\mathcal{M}^{i}}(\mathcal{S}\cup\\{f\\})-\nu^{\mathcal{M}^{i}}(\mathcal{S})\neq
0$. Combining the last two statements with _Triviality_ , we get that
$\phi(\nu^{\mathcal{M}^{i}},f_{i})\neq 0$.

To conclude, $\forall
i\in\\{0,1\\},\phi(\nu^{\mathcal{M}^{0}},f_{i})\neq\phi(\nu^{\mathcal{M}^{1}},f_{i})$,
in contradiction to the _Data-Model Equivalence_ property. $\Box$

###  3.3 Reasoning for feature importance

Feature importance is often used, even if not stated explicitly, as a proxy
for the causal analysis. Unfortunately, known difficulties from the field of
causality also arise when calculating feature importance. The example we used
to prove the inconsistency of the data-model often appears in real-world
problems. Two features can be highly similar because a common, unobserved
factor, caused them, or one of them caused the other. In other cases, features
may be highly correlated because they are both proxies for another variable,
For example, when continuously measuring a variable of interest but recording
only its mean or maximum values in discretized time points. This problem of
lacking information to disentangle the effect of two variables, is known as
non-identifiability.

To illustrate this in our context, consider two penalized regression models
that are trained on two identical features. The first model employs an L1
regularization, also known as lasso regression; and the second model employs
an L2 regularization, also known as ridge regression. The predictions of the
two models are identical. However, the calculation of commonly used feature
important methods will lead to different results - lasso regression will
result in assigning all the importance to one of the features, whereas ridge
regression will result in assigning equal importance to both features.

Another situation that may lead to unexpected outcomes from feature importance
scores is when a collider (also known as an inverted fork) exists in the data
(18; 19). As an example, assume that the following relationships hold in the
real world (illustrated in Figure 1): Smoking cigarettes (_Smoking_) causes
cancer (_Cancer_), but also increases chewing gum consumption (_Gum_). Assume
also that doctors recommend people with earaches (_Earache_) to chew gum. Now,
imagine a researcher developing a model to predict _Cancer_ using different
subsets of the features _Gum_ and _Earache_ , but lacks information on
_Smoking_.

In a first setting, the researcher uses only the _Earache_ feature. Since
earache and cancer are independent, any value-based feature importance score
will assign zero importance to _Earache_. In a second setting, where only the
_Gum_ feature is present, the researcher will conclude that _Gum_ is an
important feature, since it is correlated with _Cancer_. In a third setting,
where a model that contains both _Earache_ and _Gum_ is considered, the
researcher will infer that _Earache_ has a non-zero importance. This results
from conditioning on _Gum_ , creating an association between _Earache_ and
_Cancer_ due to presence of a collider. Intuitively, a person who chews gum
and does not have an earache is more likely to be a smoker, and hence at high
risk of cancer. Therefore, the feature importance score might mislead a naïve
researcher into thinking that earaches are predictive of cancer.

The situations described here have been studied in the causality literature
and there is no recipe for overcoming them that does not involve additional
information about the world (18; 19).

_Smoking (unobserved)_ _Gum_ _Earache_ _Cancer_ Figure 1: An example of a
directed acyclic graph with a collider variable _Gum_.

##  4 Seperable sets

In the previous section we presented several inherent inconsistencies and
limitations of feature importance scores. In this section, we present a
special scenario where these problems do not apply. The main observation is
that problems emerged when the data contained dependencies between features
with respect to the target.

Therefore, we propose a feature importance framework that assigns scores to
sets of features, rather than to single features. We will demonstrate that for
sets that have inter-set independence, this feature importance framework
manages to overcome the previously described obstacles. We note, moreover,
that when applied to inter-independent sets, many popular methods for
calculating feature importance, including those presented in Table 1, merge.

Inspired by the notion of inessential games (29; 30; 31), we propose the
following definitions to partition the feature space into separable sets:

######  Definition 4.1 (Separable set)

$\mathcal{S}\subseteq\mathcal{F}$ is separable with respect to $\nu$, if:

$\forall
T\subseteq\mathcal{F},~{}~{}~{}\nu(T)=\nu(T\cap\mathcal{S})+\nu(T\setminus\mathcal{S})$

A set $\mathcal{S}$ is separable with respect to $\nu$ if the value of any set
$T$ is the sum of the value of its intersection with $\mathcal{S}$ and the
value of the part of $T$ that is complementary to $S$. Next, we define a
partition of the feature space into separable sets.

######  Definition 4.2 (Partitioning to separable sets)

$\mathcal{G}$ is a partition of $\mathcal{F}$ to separable sets w.r.t $\nu$ if
$\mathcal{G}$ is a collection of disjoint subsets of $\mathcal{F}$ which are
separable w.r.t $\nu$, and $\bigcup_{g\in\mathcal{G}}g=\mathcal{F}$.

For a partition of $\mathcal{F}$ to separable sets $\mathcal{G}$, we consider
every set $g\in\mathcal{G}$ as a meta-feature. For a subset of meta-features
$G\subseteq\mathcal{G}$ we can denote a subset of feature
$\mathcal{S}\subseteq\mathcal{F}$ s.t $\mathcal{S}=\bigcup_{g\in
G}\bigcup_{f\in g}f$. The separable set property implies that
$\nu(\mathcal{S})=\sum_{g\in G}\nu(g)$. Hence, we can extend $\nu$ to operate
on subsets of meta-features, by defining, for $G\subseteq\mathcal{G}$, that
$\nu(G)=\sum_{g\in G}\nu(g)$. Using the terminology of Kumar et al. (31),
$\nu$ induces an inessential game with respect to $\mathcal{G}$.

A useful property of a separable partitioning is that a there exists a unique
maximal partition.

###### Theorem 3

There exists a maximal unique partition to separable sets $\mathcal{G}^{*}$
such that for any other partition to separable sets $\mathcal{G}$,
$|\mathcal{G}|<|\mathcal{G}^{*}|$. Moreover, for every separable set
$\mathcal{S}\subseteq\mathcal{F}$ there exists $G\subseteq\mathcal{G}^{*}$
such that $\mathcal{S}=\bigcup_{g\in G}\bigcup_{f\in g}f$.

The proof uses the following three lemmas, the proofs of which are attached in
the supplementary material section.

###### Lemma 3

If $\mathcal{S}\subseteq\mathcal{F}$ is a separable set, then
$\mathcal{F}\setminus\mathcal{S}$ is also a separable set.

###### Lemma 4

If $\mathcal{S}_{1},\mathcal{S}_{2}\subseteq\mathcal{F}$ are separable sets,
then $\mathcal{S}_{1}\cup\mathcal{S}_{2}$ is a separable set.

###### Lemma 5

If $\mathcal{S}_{1},\mathcal{S}_{2}\subseteq\mathcal{F}$ are separable sets,
then $\mathcal{S}_{1}\cap\mathcal{S}_{2}$ is a separable set.

Using these three lemmas we are proving the main theorem:

Proof.  [of Theorem 3]

For every feature $f\in\mathcal{F}$ let $\mathcal{S}_{f}$ be the intersection
of all separable sets that contain $f$. Note that since $\mathcal{F}$ by
itself is a separable set then this intersection is well defined.

From Lemma 5 it follows that $\mathcal{S}_{f}$ is a separable set. Moreover,
from the definition of $\mathcal{S}_{f}$ it follows that for two features
$f_{1},f_{2}\in\mathcal{F}$ we have that either
$\mathcal{S}_{f_{1}}\cap\mathcal{S}_{f_{2}}=\emptyset$ or
$\mathcal{S}_{f_{1}}=\mathcal{S}_{f_{2}}$.

Let $\mathcal{G}^{*}$ be the collection of unique $\mathcal{S}_{f}$’s.
$\mathcal{G}^{*}$ is a partition of $\mathcal{F}$ to separable sets since it
is made of disjoint separable sets which cover $\mathcal{F}$.

For any separable set $\mathcal{S}^{\prime}\subseteq\mathcal{F}$ we have that
$\mathcal{S}^{\prime}=\bigcup_{\\{f\in\mathcal{S}^{\prime}\\}}\mathcal{S}_{f}$
which completes the proof. $\Box$

###### Theorem 4

For a partitioning of $\mathcal{F}$ to separable sets $\mathcal{G}$, the
following properties hold:

  1. 1.

The feature importance scores defined in Table 1 are identical

  2. 2.

$(\phi,\nu)$ is local global consistent (i.e. Definitions 2.1,2.2 hold)

  3. 3.

The Triviality property holds (2.3) for any value-functions that satisfy
$\nu(\emptyset)=0$.

Proof.  If $\mathcal{G}$ is a partition of $\mathcal{F}$ into separable sets,
it holds that $\forall g\in\mathcal{G}$

  1. 1.

MCI, Shapley and ablation are identical to the bivariate-association function.

     * •

Ablation:

$\displaystyle\phi(\nu,g):=\nu(\mathcal{G})-\nu(\mathcal{G}\setminus\\{g\\})=\nu(\mathcal{G}\cap
g)+\nu(\mathcal{G}\setminus g)-\nu(\mathcal{G}\setminus g)=\nu(g)$

     * •

Shapley:

$\displaystyle\phi(\nu,g):=\sum_{\mathcal{S}\subseteq\mathcal{G}\setminus\\{g\\}}\Delta_{\mathcal{S}}\cdot(\nu(\mathcal{S}\cup\\{g\\})-\nu(\mathcal{S}))\hskip
102.42992pt$ $\displaystyle\hskip
31.29802pt=\sum_{\mathcal{S}\subseteq\mathcal{G}\setminus\\{g\\}}\Delta_{\mathcal{S}}\cdot(\nu((\mathcal{S}\cup\\{g\\})\cap
g)+(\nu((\mathcal{S}\cup\\{g\\})\setminus g))-\nu(\mathcal{S}))$
$\displaystyle\hskip
31.29802pt=\nu(g)\cdot\sum_{\mathcal{S}\subseteq\mathcal{G}\setminus\\{g\\}}\Delta_{\mathcal{S}}=\nu(g)$

where
$\sum_{\mathcal{S}\subseteq\mathcal{G}\setminus\\{g\\}}\Delta_{\mathcal{S}}=1$
for
$\Delta_{\mathcal{S}}:=\frac{|\mathcal{S}|!(|\mathcal{G}|-|\mathcal{S}|-1)!}{|\mathcal{G}|!}$.

     * •

MCI:

$\displaystyle\phi(\nu,g):=\max_{\mathcal{S}\subseteq\mathcal{G}\setminus\\{g\\}}(\nu(\mathcal{S}\cup\\{g\\})-\nu(\mathcal{S}))\hskip
130.88268pt$ $\displaystyle\hskip
31.29802pt=\max_{\mathcal{S}\subseteq\mathcal{G}\setminus\\{g\\}}(\nu((\mathcal{S}\cup\\{g\\})\cap
g)+\nu((\mathcal{S}\cup\\{g\\})\setminus g)-\nu(\mathcal{S}))=\nu(g)$

  2. 2.

$(\phi,\nu)$ is local-global consistent:

$\displaystyle\phi_{\mathbf{g}}(\nu,g)=\nu_{\mathbf{g}}(g)=\mathbb{E}[\nu_{x}(g)]=\mathbb{E}[\phi_{l}(\nu,g)]$

  3. 3.

     * •

$\forall\mathcal{S}\subseteq\mathcal{G}$,
$\nu(\mathcal{S})=\sum_{g\in\mathcal{S}}\nu(g)$ (by definition).

Hence, if $\nu(\mathcal{S})\neq 0$ then $\exists g\in\mathcal{S}$ s.t
$\nu(g)\neq 0$, and therefore by item (1) $\phi(\nu,g)\neq 0$.

     * •

If $\phi(\nu,g)\neq 0$ then again by item (1) $\nu(g)\neq 0$ and
$\nu(\emptyset)\neq\nu(\emptyset\cup\\{g\\})$.

$\Box$

We further notice several additional consequences of partitioning the feature
space into separable sets. First, the _Null Feature_ property (2.4) aligns
with _Triviality_ (2.3) and Theorem 4: If $g\in\mathcal{G}$ is a _Null
Feature_ then $\phi(\nu^{\mathcal{M}},g)=0$. The contraposition of the first
item of _Triviality_ implies that $\exists G\subseteq\mathcal{G}$ s.t $g\in G$
and $\nu^{\mathcal{M}}(G)=0$. This aligns with the first item of Theorem 4:
$\phi(\nu^{\mathcal{M}},g)=0\Rightarrow\nu^{\mathcal{M}}(g)=0$.

Second, we notice that the proof that $(\phi,\nu)$ is data-model inconsistent
breaks: co-linear features which are not null features, as in our example,
will always be grouped into the same set since they are dependent and
therefore they will not harm the data-model consistency.

Finally, the practical issues we raised in 3.3 no longer hold. Identical
features, in any partition to separable sets, will always be in the same
separable set, so assigning them different feature importance scores is
impossible. As for the example of the collider / inverted fork, one of the two
must occur: either both Earache and Gum will be in the same separable set, and
Earache will not have a separate score. Or, they will be in different
separable sets, which will cause the importance of Earache to be zero, as
easily seen by its bivariate-association importance.

##  5 Conclusion

Feature importance can be categorized into four settings, along two main axes:
global vs. local and model vs. data. In this work, we attempted to create a
unified framework of feature importance, accounting for all four settings and
their interactions. We defined expected properties of feature importance
scores and the relations between them. Surprisingly, we found that it is
impossible to define feature importance scores that will be consistent between
the settings. Specifically, the expected behavior of local-global scores
contradicts previous results of the data-global setting. Furthermore, there is
no guarantee that feature importance scores of a model that perfectly predicts
the data will reflect the data feature importance.

To overcome these limitations of feature importance scores, we proposed an
alternative: assigning a single score to each set of features that has inter-
set independence with respect to their values – termed separable sets. We
showed that a unique maximal partition to separable sets exists, and that the
demonstrated limitations of feature importance do not apply when using these
sets as meta-features. We note that other methods previously proposed
assigning a score to every set of features of size $k$ (31; 32). In contrast,
our partition does not prespecificy a set size, nor demands a constant size
for each separable set. It relies on the data structure to create sets that
yield a consistent feature importance score. Separable sets also possess the
advantage that common feature importance scores unify on them, dismissing the
need to select a certain score. The number of separable sets is bounded by the
number of features, therefore avoiding the complexity associated with
presenting ${|\mathcal{F}|\choose k}$ scores to the user. However, we do not
present an explicit way to re-partition the feature space into separable sets.
Achieving such a re-partition, or at least the maximal partition, may prove to
be of high computational complexity. Future work should explore methods of
finding and optimizing the partition of the feature space into separable sets.

We do not argue that we have defined the only possible set of relevant
properties for the various settings. We did, however, attempt to define a
minimal set of properties that we believe are essential. Yet, even these
requirements led to inconsistencies. It could be argued that the
inconsistencies we identified are invalid, because our assumptions are flawed.
For example, the assumptions made by Catav et al. (7) may not be convincing.
Or, the assumption that the global score matches the expectancy of the local
score is not a proper way to establish consistency between the settings.
Despite these potential pitfalls, we believe that our work contains
theoretical developments that integrate previously isolated concepts of
feature importance scores.

Our results show that feature importance scores should be used cautiously,
responsibly and ethically, to prevent naive researchers and users from
reaching incorrect conclusions. This is aligned with recent research that
tries to measure the quality of explainability tools and their usefulness for
different applications (33; 34; 35). A possible negative consequence of this
study might be attenuating the trust in explainable AI. However, our work
promotes substantive discussions and accurate definitions of explainability,
as previously advocated (21; 17). We hope that our work will contribute to
stimulating additional research that will result in solid foundations for
explainable AI.

## References

  * Shapley (1953) Lloyd S Shapley.  A value for n-person games.  _Contributions to the Theory of Games_ , 2(28):307–317, 1953.
  * Casagrande and Diamond (1974) VA Casagrande and IT Diamond.  Ablation study of the superior colliculus in the tree shrew (tupaia glis).  _Journal of Comparative Neurology_ , 156(2):207–237, 1974.
  * Bengtson and Roth (2008) Eric Bengtson and Dan Roth.  Understanding the value of features for coreference resolution.  In _Proceedings of the 2008 Conference on Empirical Methods in Natural Language Processing_ , pages 294–303, Honolulu, Hawaii, October 2008. Association for Computational Linguistics.  URL https://www.aclweb.org/anthology/D08-1031.
  * Hessel et al. (2018) Matteo Hessel, Joseph Modayil, Hado Van Hasselt, Tom Schaul, Georg Ostrovski, Will Dabney, Dan Horgan, Bilal Piot, Mohammad Azar, and David Silver.  Rainbow: Combining improvements in deep reinforcement learning.  In _Thirty-Second AAAI Conference on Artificial Intelligence_ , 2018\.
  * Covert et al. (2020) Ian Covert, Scott Lundberg, and Su-In Lee.  Understanding global feature contributions with additive importance measures.  _Advances in Neural Information Processing Systems_ , 33, 2020.
  * Lundberg and Lee (2017) Scott M Lundberg and Su-In Lee.  A unified approach to interpreting model predictions.  In _Advances in neural information processing systems_ , pages 4765–4774, 2017.
  * Catav et al. (2021) Amnon Catav, Boyang Fu, Yazeed Zoabi, Ahuva Libi Weiss Meilik, Noam Shomron, Jason Ernst, Sriram Sankararaman, and Ran Gilad-Bachrach.  Marginal contribution feature importance-an axiomatic approach for explaining data.  In _International Conference on Machine Learning_ , pages 1324–1335. PMLR, 2021.
  * Kulesza et al. (2015) Todd Kulesza, Margaret Burnett, Weng-Keen Wong, and Simone Stumpf.  Principles of explanatory debugging to personalize interactive machine learning.  In _Proceedings of the 20th international conference on intelligent user interfaces_ , pages 126–137, 2015.
  * Tan et al. (2018) Sarah Tan, Rich Caruana, Giles Hooker, Paul Koch, and Albert Gordo.  Learning global additive explanations for neural nets using model distillation.  _arXiv preprint arXiv:1801.08640_ , 2018.
  * Fontana et al. (2013) Juan M Fontana, Muhammad Farooq, and Edward Sazonov.  Estimation of feature importance for food intake detection based on random forests classification.  In _2013 35th Annual International Conference of the IEEE Engineering in Medicine and Biology Society (EMBC)_ , pages 6756–6759. IEEE, 2013\.
  * Danaee et al. (2017) Padideh Danaee, Reza Ghaeini, and David A Hendrix.  A deep learning approach for cancer detection and relevant gene identification.  In _Pacific symposium on biocomputing_ , pages 219–229. World Scientific, 2017.
  * McKinney et al. (2006) Brett A McKinney, David M Reif, Marylyn D Ritchie, and Jason H Moore.  Machine learning for detecting gene-gene interactions.  _Applied bioinformatics_ , 5(2):77–88, 2006.
  * Haljas et al. (2018) Kadri Haljas, Azmeraw T Amare, Behrooz Z Alizadeh, Yi-Hsiang Hsu, Thomas Mosley, Anne Newman, Joanne Murabito, Henning Tiemeier, Toshiko Tanaka, Cornelia Van Duijn, et al.  Bivariate genome-wide association study of depressive symptoms with type 2 diabetes and quantitative glycemic traits.  _Psychosomatic medicine_ , 80(3):242, 2018.
  * Karlaš et al. (2022) Bojan Karlaš, David Dao, Matteo Interlandi, Bo Li, Sebastian Schelter, Wentao Wu, and Ce Zhang.  Data debugging with shapley importance over end-to-end machine learning pipelines.  _arXiv preprint arXiv:2204.11131_ , 2022.
  * Guo et al. (2018) Wenbo Guo, Dongliang Mu, Jun Xu, Purui Su, Gang Wang, and Xinyu Xing.  Lemna: Explaining deep learning based security applications.  In _Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security_ , pages 364–379, 2018.
  * Lundberg et al. (2020) Scott M Lundberg, Gabriel Erion, Hugh Chen, Alex DeGrave, Jordan M Prutkin, Bala Nair, Ronit Katz, Jonathan Himmelfarb, Nisha Bansal, and Su-In Lee.  From local explanations to global understanding with explainable ai for trees.  _Nature machine intelligence_ , 2(1):2522–5839, 2020.
  * Lipton (2018) Zachary C Lipton.  The mythos of model interpretability.  _Queue_ , 16(3):31–57, 2018.
  * Pearl (2009) Judea Pearl.  _Causality_.  Cambridge university press, 2009.
  * Hernán and Robins (2010) Miguel A Hernán and James M Robins.  Causal inference, 2010.
  * Chen et al. (2020) Hugh Chen, Joseph D Janizek, Scott Lundberg, and Su-In Lee.  True to the model or true to the data?  _arXiv preprint arXiv:2006.16234_ , 2020.
  * Kumar et al. (2020) I Elizabeth Kumar, Suresh Venkatasubramanian, Carlos Scheidegger, and Sorelle Friedler.  Problems with shapley-value-based explanations as feature importance measures.  In _International Conference on Machine Learning_ , pages 5491–5500. PMLR, 2020.
  * Frye et al. (2020) Christopher Frye, Colin Rowat, and Ilya Feige.  Asymmetric shapley values: incorporating causal knowledge into model-agnostic explainability.  _Advances in Neural Information Processing Systems_ , 33, 2020.
  * Janzing et al. (2020) Dominik Janzing, Lenon Minorics, and Patrick Blöbaum.  Feature relevance quantification in explainable ai: A causal problem.  In _International Conference on artificial intelligence and statistics_ , pages 2907–2916. PMLR, 2020.
  * Zien et al. (2009) Alexander Zien, Nicole Krämer, Sören Sonnenburg, and Gunnar Rätsch.  The feature importance ranking measure.  In _Joint European Conference on Machine Learning and Knowledge Discovery in Databases_ , pages 694–709. Springer, 2009.
  * Ribeiro et al. (2016) Marco Tulio Ribeiro, Sameer Singh, and Carlos Guestrin.  " why should i trust you?" explaining the predictions of any classifier.  In _Proceedings of the 22nd ACM SIGKDD international conference on knowledge discovery and data mining_ , pages 1135–1144, 2016.
  * Selvaraju et al. (2017) Ramprasaath R Selvaraju, Michael Cogswell, Abhishek Das, Ramakrishna Vedantam, Devi Parikh, and Dhruv Batra.  Grad-cam: Visual explanations from deep networks via gradient-based localization.  In _Proceedings of the IEEE international conference on computer vision_ , pages 618–626, 2017.
  * Bach et al. (2015) Sebastian Bach, Alexander Binder, Grégoire Montavon, Frederick Klauschen, Klaus-Robert Müller, and Wojciech Samek.  On pixel-wise explanations for non-linear classifier decisions by layer-wise relevance propagation.  _PloS one_ , 10(7):e0130140, 2015.
  * Janssen and Guan (2022) Joseph Janssen and Vincent Guan.  Ultra marginal feature importance.  _arXiv preprint arXiv:2204.09938_ , 2022.
  * Bird (1975) Charles Bird.  Inessential games and non-imposed solutions to allocation problems.  _Public Choice_ , 22(1):91–102, 1975.
  * Stern and Tettenhorst (2019) Ari Stern and Alexander Tettenhorst.  Hodge decomposition and the shapley value of a cooperative game.  _Games and Economic Behavior_ , 113:186–198, 2019.
  * Kumar et al. (2021) Indra Kumar, Carlos Scheidegger, Suresh Venkatasubramanian, and Sorelle Friedler.  Shapley residuals: Quantifying the limits of the shapley value for explanations.  _Advances in Neural Information Processing Systems_ , 34, 2021.
  * Sundararajan et al. (2020) Mukund Sundararajan, Kedar Dhamdhere, and Ashish Agarwal.  The shapley taylor interaction index.  In _International conference on machine learning_ , pages 9259–9268. PMLR, 2020.
  * Rudin and Radin (2019) Cynthia Rudin and Joanna Radin.  Why are we using black box models in ai when we don’t need to? a lesson from an explainable ai competition.  2019\.
  * Chang et al. (2021) Chun-Hao Chang, Sarah Tan, Ben Lengerich, Anna Goldenberg, and Rich Caruana.  How interpretable and trustworthy are gams?  In _Proceedings of the 27th ACM SIGKDD Conference on Knowledge Discovery & Data Mining_, pages 95–105, 2021.
  * Visani et al. (2022) Giorgio Visani, Enrico Bagli, Federico Chesani, Alessandro Poluzzi, and Davide Capuzzo.  Statistical stability indices for lime: Obtaining reliable explanations for machine learning models.  _Journal of the Operational Research Society_ , 73(1):91–101, 2022.

##  Appendix A Appendix

###  A.1 Properties of the data setting

In this section we attach the settings from Catav et al. [2021], which we
followed in the definition of the data-global setting.

The properties use the Elimination operation, which is defined as follows:

###### Definition A.1

Let $\mathcal{F}$ be a set of features and $\nu$ be a value-function.
Eliminating the set $T\subset\mathcal{F}$ creates a new set of features
$\mathcal{F}^{\prime}=\mathcal{F}\setminus T$ and a new value-function
$\nu^{\prime}:\mathcal{F}^{\prime}\rightarrow\mathbb{R}^{+}$ such that
$\forall\mathcal{S}\subseteq\mathcal{F}^{\prime},\nu^{\prime}(\mathcal{S})=\nu(\mathcal{S})$

Using this definition, the set of required properties is as follows:

###### Definition A.2

A valid feature importance function $\phi(\nu)$ in the data-global setting is
a function $\phi:2^{|\mathcal{F}|}\rightarrow\mathbb{R}^{+}$ that has the
following properties:

  1. 1.

Marginal Contribution:  The importance of a feature is equal or higher than
the increase in the evaluation function when adding it to all the other
features, i.e

$\phi(\nu,f)\geq\nu(\mathcal{F})-\nu(\mathcal{F}\setminus{f})).$

  2. 2.

Elimination:  Eliminating features from $\mathcal{F}$ can only decrease the
importance of each feature. i.e., if $T\subseteq\mathcal{F}$ and
$\nu^{\prime}$ is the value-function which is obtained by eliminating $T$ from
$\mathcal{F}$ then

$\forall f\in\mathcal{F}\setminus T,\phi(\nu,f)\geq\phi(\nu^{\prime},f).$

  3. 3.

Minimalism:  If $\phi(\nu)$ is the feature importance function, then for every
function $\phi^{\prime}:2^{|\mathcal{F}|}\rightarrow\mathbb{R}^{+}$ for which
axioms 1 and 2 hold, and for every $f\in\mathcal{F}$:
$\phi(\nu,f)\leq\phi^{\prime}(\nu,f)$

###  A.2 Proofs for Lemmas 1,2

When proving the inconsistency between the local and the global settings, we
used two lemmas. The first lemma stated that if the consistency holds between
the local and the global, then the local function is identical to the the
global function. The second lemma stated that if the consistency holds, then
the global function is linear. The proof for these lemmas appears below:

Proof. [of Lemma 1]

Assume, in contradiction, that $\exists x\in\mathcal{X}$ s.t
$\phi_{\mathbf{g}}(\nu_{x})\neq\phi_{l}(\nu_{x})$. It holds that

$\phi_{\mathbf{g}}(\nu_{\mathbf{g}})=\phi_{\mathbf{g}}(\mathbb{E}[\nu_{x}])=\mathbb{E}[\phi_{l}(\nu_{x})]$

We construct a new sample space $\mathcal{X}_{x}$ comprised solely of
duplicates of $x$ , i.e $\forall
x\in\mathcal{X}_{x},\nu_{x}\equiv\nu_{\mathbf{g}}$. It implies that $\forall
x^{\prime}\in\mathcal{X}_{x}$,

$\phi_{\mathbf{g}}(\nu_{x^{\prime}})=\phi_{l}(\nu_{x^{\prime}})$

in contradiction to our assumption. $\Box$

Proof. [of Lemma 2]

Let $\alpha\in[0,1]$, and let $x_{1},x_{2}\in\mathcal{X}$. We construct a new
sample space $\mathcal{X}_{1,2}$ s.t consisting of
$\alpha\cdot|\mathcal{X}_{1,2}|$ duplicates of $x_{1}$ and
$(1-\alpha)\cdot|\mathcal{X}_{1,2}|$ duplicates of $x_{2}$. it holds that

$\displaystyle\alpha\cdot\phi_{\mathbf{g}}(\nu_{x_{1}})+(1-\alpha)\cdot\phi_{\mathbf{g}}(\nu_{x_{2}})=$
(1)
$\displaystyle\alpha\cdot\phi_{l}(\nu_{x_{1}})+(1-\alpha)\cdot\phi_{l}(\nu_{x_{2}})=$
(2) $\displaystyle\mathbb{E}[\phi_{l}(\nu_{x})]=$ (3)
$\displaystyle\phi_{\mathbf{g}}(\mathbb{E}[\nu_{x}])=$ (4)
$\displaystyle\phi_{\mathbf{g}}(\alpha\cdot\nu_{x_{1}}+(1-\alpha)\cdot\nu_{x_{2}})\hskip
28.45274pt$ (5)

where (2) is valid by lemma 1, (3) and (5) are valid by the expected value of
$\mathcal{X}_{1,2}$, and (4) is valid by the consistency property. $\Box$

###  A.3 Counter example for Theorem 1

This counter-example proves that MCI is not a linear function, thus leading to
a contradiction between the definitions of the data-global setting and the
lemma that proved that the global function is linear. In doing so, we
demonstrate a contradiction to the claim of consistency between the local and
the global settings.

$\displaystyle\alpha\cdot MCI(\nu_{x_{1}})+(1-\alpha)\cdot
MCI(\nu_{x_{2}})\neq MCI(\alpha\cdot\nu_{x_{1}}+(1-\alpha)\cdot\nu_{x_{2}})$
(6)

Let $\alpha=\frac{1}{2}$ and let $x_{0},x_{1}\in\mathcal{X}_{1,2}$ be a
dataset of instances composed of two features $f_{0},f_{1}$ such that

$\nu_{x_{0}}:=$ $\begin{pmatrix}\\{\emptyset\\}:=0\\\ \\{f_{0}\\}:=0\\\
\\{f_{1}\\}:=1\\\ \\{f_{0},f_{1}\\}:=2\\\
\end{pmatrix},\nu_{x_{1}}:=\begin{pmatrix}\\{\emptyset\\}:=0\\\
\\{f_{0}\\}:=1\\\ \\{f_{1}\\}:=1\\\ \\{f_{0},f_{1}\\}:=1\\\ \end{pmatrix}$.

On one hand,

$\displaystyle\frac{1}{2}\cdot MCI(\begin{pmatrix}0\\\ 0\\\ 1\\\
2\end{pmatrix})+\frac{1}{2}\cdot MCI(\begin{pmatrix}0\\\ 1\\\ 1\\\
1\end{pmatrix})=\frac{1}{2}\cdot\begin{pmatrix}1\\\ 2\\\
\end{pmatrix}+\frac{1}{2}\cdot\begin{pmatrix}1\\\ 1\\\
\end{pmatrix}=\begin{pmatrix}1\\\ 1.5\\\ \end{pmatrix}$

On the other hand,

$\displaystyle MCI(\frac{1}{2}\cdot\begin{pmatrix}0\\\ 0\\\ 1\\\
2\end{pmatrix}+\frac{1}{2}\cdot\begin{pmatrix}0\\\ 1\\\ 1\\\
1\end{pmatrix})=MCI(\begin{pmatrix}0\\\ 0.5\\\ 1\\\
1.5\end{pmatrix})=\begin{pmatrix}0.5\\\ 1\\\ \end{pmatrix}$

Hence, we found a counter example consistent with (6), which contradicts the
linearity of MCI.

###  A.4 Proofs for Lemmas 3,4, and 5

In proving that there exists a maximal and unique partitioning of
$\mathcal{F}$ into separable sets, we used three lemmas: The first lemma
stated that if a set is a separable set, then so is its complement. The second
lemma stated that if two sets are separable, so is their union. The third
lemma stated that for two separable sets, their intersection is also a
separable set. The proofs for the lemmas appear below:

Proof. [of Lemma 3]

The proof follows immediately from the definition. $\Box$

Proof. [of Lemma 4]

For a set $T,\mathcal{S}_{1},\mathcal{S}_{2}\subseteq\mathcal{F}$ it holds
that

$\displaystyle\nu(T)=\nu(T\cap\mathcal{S}_{1})+\nu(T\setminus\mathcal{S}_{1})=\nu(T\cap\mathcal{S}_{1})+\nu((T\setminus\mathcal{S}_{1})\cap\mathcal{S}_{2})+\nu((T\setminus(\mathcal{S}_{1}\cup\mathcal{S}_{2}))$
$\displaystyle\nu(T\cap(\mathcal{S}_{1}\cup\mathcal{S}_{2}))=\nu(T\cap(\mathcal{S}_{1}\cup\mathcal{S}_{2})\cap\mathcal{S}_{1})+\nu(T\cap(\mathcal{S}_{1}\cup\mathcal{S}_{2})\setminus\mathcal{S}_{1})=\nu(T\cap\mathcal{S}_{1})+\nu(T\setminus\mathcal{S}_{1})\cap\mathcal{S}_{2})$
Therefore,
$\displaystyle\nu(T)=\nu(T\cap\mathcal{S}_{1})+\nu((T\setminus\mathcal{S}_{1})\cap\mathcal{S}_{2})+\nu((T\setminus\mathcal{S}_{1})\setminus\mathcal{S}_{2})=\nu(T\cap(\mathcal{S}_{1}\cup\mathcal{S}_{2}))+\nu(T\setminus(\mathcal{S}_{1}\cup\mathcal{S}_{2}))$

$\Box$

Proof. [of Lemma 5]

From Lemmas 3-4 we have that
$(\mathcal{F}\setminus\mathcal{S}_{1})\cup(\mathcal{F}\setminus\mathcal{S}_{2})$
is a separable set.

By the fact that
$(\mathcal{F}\setminus\mathcal{S}_{1})\cup(\mathcal{F}\setminus\mathcal{S}_{2})=\mathcal{F}\setminus(\mathcal{S}_{1}\cap\mathcal{S}_{2})$
we get that $\mathcal{F}\setminus(\mathcal{S}_{1}\cap\mathcal{S}_{2})$ is a
separable set.

Using Lemma 1 again, we get that $\mathcal{S}_{1}\cap\mathcal{S}_{2}$ is a
separable set, as required. $\Box$

###  A.5 Toy example of separable sets

Here, we illustrate the effects of assigning importance scores to separable
sets in the data-global setting. We construct an example in which different
feature importance methods disagree on the importance of features. Then, we
partition the feature space into separable sets. Consequently, the different
feature importance methods merge when applied to these separable sets.

We take the value-function to be the coefficient of determination of a linear
regression model without an intercept, i.e.
$\forall\mathcal{S}\subseteq\mathcal{F},\nu(\mathcal{S})=1-\sum_{i}(\hat{y}^{\mathcal{S}}_{i}-y_{i})^{2}/\sum_{i}y_{i}^{2}$,
where $\hat{y}^{\mathcal{S}}_{i}$ is the prediction for instance $y_{i}$
restricted to the feature subset $\mathcal{S}$. This is a common metric of
assessing a model’s fit to a continuous target variable.

Assume the world consists of three features, determining the target variable:
$y=f_{1}+f_{3}+U$. Also, assume that we observe only $f_{1},f_{2}$, $f_{3}$,
while $U$ is a source of unexplained variance. We consider the following
dataset:

$\blockarray{ccccr}&f_{1}f_{2}f_{3}U\\\ \block{c(cccr)}x_{1}11-1\hskip
5.69054pt\sqrt{\frac{1}{6}}\\\ x_{2}110-\sqrt{\frac{2}{3}}\\\ x_{3}111\hskip
5.69054pt\sqrt{\frac{1}{6}}\\\ $

Note that these features were selected to be orthogonal, besides $f_{1}$ and
$f_{2}$ which are duplicates.

For the observed feature space, the value-function is as follow:

$\nu(\mathcal{S})=\begin{cases}0,\hskip 49.50777pt\mathcal{S}=\emptyset\\\
\nicefrac{{1}}{{2}},\hskip 42.67912pt\mathcal{S}=f_{1}\\\
\nicefrac{{1}}{{2}},\hskip 42.67912pt\mathcal{S}=f_{2}\\\
\nicefrac{{1}}{{3}},\hskip 42.67912pt\mathcal{S}=f_{3}\\\
\nicefrac{{1}}{{2}},\hskip 42.67912pt\mathcal{S}=\\{f_{1},f_{2}\\}\\\
\nicefrac{{5}}{{6}},\hskip 42.67912pt\mathcal{S}=\\{f_{1},f_{3}\\}\\\
\nicefrac{{5}}{{6}},\hskip 42.67912pt\mathcal{S}=\\{f_{2},f_{3}\\}\\\
\nicefrac{{5}}{{6}},\hskip
42.67912pt\mathcal{S}=\\{f_{1},f_{2},f_{3}\\}\end{cases}$

Therefore, we can easily see that the common methods for calculating feature
importance produce different results:

  * •

Ablation assigns each of the duplicates features $f_{1},f_{2}$ with zero
importance.

  * •

For Shapley, each duplicate feature has a non-zero importance, but as we
introduce more duplicates, their importance decreases.

  * •

The bivariate feature importance and MCI assign $\nicefrac{{1}}{{2}}$
importance to each of the duplicate features, and do not change this value
upon introduction of additional duplicates.

On the other hand, we can see that $\\{f_{1},f_{2}\\}$ and $f_{3}$ are
separable sets w.r.t $\nu$. By partitioning the feature space into
$\mathcal{G}:=\\{\\{f_{1},f_{2}\\},f_{3}\\}$, all the feature importance
functions mentioned above yield

$\phi(\nu,g)=\begin{cases}\nicefrac{{1}}{{2}},\hskip
42.67912ptg=\\{f_{1},f_{2}\\}\\\ \nicefrac{{1}}{{3}},\hskip
42.67912ptg=f_{3}\end{cases}$

###  A.6 Additional properties

In this work we presented a framework that consist of a small set of
properties for the various settings of feature importance. For the sake of
completeness, we present here additional properties that were not required for
our results, but might be useful for future work:

######  Definition A.3 (Empty-Set Value)

$\nu(\emptyset)=0$

The _Empty-Set Value_ property is a technical property that aims to prevent
edge cases.

######  Definition A.4 (Monotonicity)

The Monotonicity property holds if:

  * •

$\forall\mathcal{S}_{1},\mathcal{S}_{2}\subseteq\mathcal{F}$ s.t
$\mathcal{S}_{2}\subseteq\mathcal{S}_{1}$, it holds that
$\nu_{\mathbf{g}}(\mathcal{S}_{2})\leq\nu_{\mathbf{g}}(\mathcal{S}_{1})$

The _Monotonicity_ property states that the value in the global setting of
each subset is less than or equal to the value of each set in which it is
contained.

Notice that the _Monotonicity_ property is defined only for the global
setting. There are cases where the value of a local instance might not be
monotonic. Also, we observe that _Empty-set Value_ and _Monotonicity_ imply
non-negativity for the value-function in the global setting.

######  Definition A.5 (Symmetry)

The symmetry property holds if $\forall f_{1},f_{2}\in\mathcal{F}$:

  * •

If $\forall\mathcal{S}\subseteq\mathcal{F}\setminus z$ it holds that
$\nu(\mathcal{S}\cup\\{f_{1}\\})=\nu(\mathcal{S}\cup\\{f_{2}\\})$ then

$\phi(\nu,f_{1})=\phi(\nu,f_{2})$

where z can be defined as $\emptyset$ or $\\{f_{1},f_{2}\\}$.

The _Symmetry_ property states that if two features are identical in their
contribution to each subset with respect to the value, their importance should
be identical. Using $z$ one can define two different definitions of symmetry,
both of which are accepted in the literature.

######  Corollary 1 (Triviality)

The Triviality property implies that $\forall f\in\mathcal{F}$:

  * •

If $\forall\mathcal{S}\subseteq\mathcal{F},\nu(\mathcal{S}\cup
f)=\nu(\mathcal{S})$ then $\phi(\nu,f)=0$

This corollary to the _Triviality_ property aims to emphasize an important
trait of this property.

######  Definition A.6 (Separable Importance)

The separable importance property consists of two parts:

  1. 1.

If $\mathcal{S}$ is a separable set w.r.t $\nu$, then $\forall
f\in\mathcal{F},\phi(\nu,f)=\phi^{\mathcal{S}}(\nu,f)+\phi^{\mathcal{F}\setminus\mathcal{S}}(\nu,f)$

  2. 2.

If $\forall
f\in\mathcal{F},\phi(\nu,f)=\phi^{\mathcal{S}}(\nu,f)+\phi^{\mathcal{F}\setminus\mathcal{S}}(\nu,f)$
then $\mathcal{S}$ is a separable set w.r.t $\nu$.

where $\phi^{\mathcal{S}}$ denotes the feature importance function restricted
to the subset $\mathcal{S}$.

The first item of the _Separable Importance_ property claims that if a set is
separable, the importance function can also be separated with respect to this
set. The second item of the _Separable Importance_ property states that if the
importance function can be separated with respect to a set, this set is a
separable set.


# On Program Completion, with an Application
to the Sum and Product Puzzle

Vladimir Lifschitz
University of Texas

###### Abstract

This paper describes a generalization of Clark’s completion that is applicable
to logic programs containing arithmetic operations and produces syntactically
simple, natural looking formulas. If a set of first-order axioms is equivalent
to the completion of a program then we may be able to find standard models of
these axioms by running an answer set solver. As an example, we apply this
“reverse completion” procedure to the Sum and Product Puzzle.

##  1 Introduction

Program completion [Clark (1978), Lloyd and Topor (1984)] is a transformation
that converts logic programs into sets of first-order formulas. The study of
completion improved our understanding of the relationship between these two
knowledge representation formalisms, and it has been used in the design of
answer set solvers [Lierler and Maratea (2004), Lin and Zhao (2004)].

The definition of completion has been extended to programs with operations on
integers [Fandinno et al. (2020)]. That generalized completion process
produces formulas in a two-sorted first-order language [Lifschitz et al.
(2019), Section 5]. In addition to “general” variables, which range over both
symbolic constants and (symbols for) integers, a formula in that language may
include also variables ranging over integers only. The need to use a language
with two sorts is explained by the fact that function symbols in a first-order
language are supposed to represent total functions, and arithmetic operations
are not defined on symbolic constants. In answer set programming languages,
applying arithmetic operations to symbolic constants is usually handled in a
different way; when a rule is instantiated, a substituition is not used unless
it is “well-formed” [Calimeri et al. (2020), Section 3].

In this paper, the idea of a natural translation [Lifschitz (2021)] is used to
define a version of generalized completion that is limited to relatively
simple (“regular”) rules but produces simpler, and more natural-looking,
formulas. The modified completion operator is denoted by NCOMP, for “natural
completion.” For example, the natural completion of the one-rule program

$\verb|even(2*X) :- X = -10..10.|$ (1)

in the input language of the answer set solver clingo [Gebser et al. (2019)]
is the sentence

$\forall V(\emph{even\/}(V)\leftrightarrow\exists I(\overline{-10}\leq
I\leq\overline{10}\,\land\,V=\overline{2}*I)).$ (2)

Here $V$ is a general variable, $I$ is an integer variable, and
$\overline{-10}$, $\overline{10}$, $\overline{2}$ are “numerals”—object
constants representing integers.

Two theorems, stated in Section 3.4 and proved in Section 5, relate stable
models of a regular program to standard models of its completion (standard in
the sense that they interpret symbols related to integers as usual in
arithmetic). These theorems extend well-known results due to François Fages
[Fages (1991)].

If a set of first-order axioms happens to be equivalent to the completion of a
regular program then we may be able to find standard models of these axioms by
running an answer set solver. As an example, we apply this “reverse
completion” procedure to a formalization of the Sum and Product Puzzle
(https://en.wikipedia.org/wiki/Sum_and_Product_Puzzle). From the perspective
of knowledge representation and automated reasoning, that puzzle presents a
challenge: express it in a formal declarative language so that the answer can
be found, or at least verified, by an automated reasoning tool. This has been
accomplished using first-order axioms for Kripke-style possible worlds and the
first-order theorem prover fol [McCarthy (1990)], and also using a modal logic
of public announcements and the epistemic model checker demo [van Ditmarsch et
al. (2005)]. More recently, Jayadev Misra proposed a simple first-order
formalization that does not refer to possible worlds [Misra (2022), Section
2.8.3]. In Section 4 we show that the answer to the puzzle can be found by
applying the reverse completion process to a variant of his axiom set and then
running clingo.

##  2 Review: rules and formulas

###  2.1 Regular rules

To simplify presentation, we do not include here some of the programming
constructs that are classified as regular in the previous publication on
natural translations [Lifschitz (2021)]. As in the Abstract Gringo article
[Gebser et al. (2015)], rules will be written in abstract notation, which
disregards some details related to representing rules by strings of ASCII
characters. For example, rule (1) will be written as

$\emph{even\/}(\overline{2}\times X)\leftarrow
X=\overline{-10}\,..\,\overline{10}.$ (3)

We assume that three disjoint countably infinite sets of symbols are selected:
_numerals_ , _symbolic constants_ , and _(general) variables_. We assume that
a 1-1 correspondence between numerals and integers is chosen; the numeral
corresponding to an integer $n$ is denoted by $\overline{n}$. _Precomputed
terms_ are numerals and symbolic constants. We assume that a total order on
the set of precomputed terms is chosen so that, for all integers $m$ and $n$,

  * •

$\overline{m}<\overline{n}$ iff $m<n$, and

  * •

every precomputed term $t$ such that $\overline{m}<t<\overline{n}$ is a
numeral.

_Regular terms_ are formed from numerals and variables using the binary
function symbols $+,\ -,\ \times$. A _regular atom_ is an expression of the
form $p({\bf t})$, where $p$ is a symbolic constant and $\bf t$ is a tuple of
symbolic constants and regular terms, separated by commas. _Regular
comparisons_ are expressions of the forms

  * •

$t_{1}\prec t_{2}$, where each of $t_{1}$, $t_{2}$ is a symbolic constant or a
regular term, and $\prec$ is one of the comparison symbols $=,\ \neq,\ <,\ >,\
\leq,\ \geq,$ and

  * •

$t_{1}=t_{2}\,..\,t_{3}$, where $t_{1},\ t_{2},\ t_{3}$ are regular terms.

A _regular rule_ is an expression of the form

$\emph{Head\/}\leftarrow\emph{Body\/}$ (4)

where

  * •

_Head_ is either a regular atom (then (4) is a _basic rule_), or a regular
atom in braces (then (4) is a _choice rule_), or empty (then (4) is a
_constraint_), and

  * •

_Body_ is a conjunction, possibly empty, of (i) regular atoms, possibly
preceded by _not_ , and (ii) regular comparisons.

For example, (3) is a regular rule.

A _regular program_ is a finite set of regular rules. This is a special case
of Abstract Gringo programs [Gebser et al. (2015)], and stable models of a
regular program are understood in the sense of the semantic of Abstract
Gringo. Thus stable models are sets of ground atoms that do not contain
arithmetic operations.

###  2.2 Two-sorted formulas

A _predicate symbol_ is a pair $p/n$, where $p$ is a symbolic constant and $n$
is a nonnegative integer. About a predicate symbol $p/n$ we say that it
_occurs_ in a regular program $\Pi$ if some atom of the form
$p(t_{1},\dots,t_{n})$ occurs in one of the rules of $\Pi$.

For any regular program $\Pi$, by $\sigma_{\Pi}$ we denote the two-sorted
signature with the sort _general_ and its subsort _integer_ , which includes

  * •

every numeral as an object constant of the sort _integer_ ,

  * •

every symbolic constant as an object constant of the sort _general_ ,

  * •

the symbols $+$, $-$, $\times$ as binary function constants with the argument
sorts _integer_ and the value sort _integer_ ,

  * •

every predicate symbol $p/n$ that occurs in $\Pi$ as an $n$-ary predicate
constant with the argument sorts _general_ ,

  * •

the symbols $\neq$, $<$, $>$, $\leq$, $\geq$ as binary predicate constants
with the argument sorts _general_.

A formula over $\sigma_{\Pi}$ that has the form $(p/n)({\bf t})$ can be
abbreviated as $p({\bf t})$. This convention allows us to view regular atoms
occurring in $\Pi$ as atomic formulas over $\sigma_{\Pi}$.

Conjunctions of equalities and inequalities can be abbreviated as usual in
algebra; for instance, $t_{1}\leq t_{2}\leq t_{3}$ stands for $t_{1}\leq
t_{2}\land t_{2}\leq t_{3}$. An equality between tuples of terms
$(t_{1},\dots,t_{k})=(t^{\prime}_{1},\dots,t^{\prime}_{k})$ is understood as
the conjunction $t_{1}=t^{\prime}_{1}\land\cdots\land t_{k}=t^{\prime}_{k}$.

In this paper, integer variables are denoted by capital letters from the
middle of the alphabet ($I,\dots,N$), and general variables by letters from
the end ($U,\dots,Z$).

##  3 Completion

###  3.1 Replacing variables

In the process of constructing the natural completion of a regular program
$\Pi$, the bodies of rules of $\Pi$ will be transformed into formulas over
$\sigma_{\Pi}$. Since general variables are not allowed in a formula in the
scope of an arithmetic operation, this process has to involve replacing some
of them by integer variables.

A _critical variable_ of a regular rule $R$ is a general variable $X$ such
that at least one occurrence of $X$ in $R$ is in the scope of an arithmetic
operation or is part of a comparison of the form $t_{1}=t_{2}\,..\,t_{3}$. For
every regular rule $R$, choose a function $f_{R}$ that maps its critical
variables to pairwise distinct integer variables. This function $f_{R}$ is
extended to other subexpressions of $R$ as follows. For a tuple $\bf t$ of
symbolic constants and regular terms, $f_{R}({\bf t})$ is the tuple of terms
over $\sigma_{\Pi}$ obtained from $\bf t$ by replacing all occurrences of
every critical variable $X$ with the integer variable $f_{R}(X)$. Applying
$f_{R}$ to a regular atom and to a comparison that does not contain intervals
is defined in a similar way. The result of applying $f_{R}$ to $\emph{not\/}\
A$ is defined as the formula $\neg f_{R}(A)$, and the result of applying
$f_{R}$ to a comparison $t_{1}=t_{2}\,..\,t_{3}$ is $f_{R}(t_{2})\leq
f_{R}(t_{1})\leq f_{R}(t_{3})$. Finally, applying $f_{R}$ to the body
$B_{1}\land B_{2}\land\cdots$ of $R$ gives the formula $f_{R}(B_{1})\land
f_{R}(B_{2})\land\cdots$.

For instance, if $R$ is rule (3) then the variable $X$ is critical, and
$f_{R}$ maps $X$ to some integer variable $I$. It transforms the term
$\overline{2}\times X$ in the head into $\overline{2}\times I$, and the body
$X=\overline{-10}\,..\,\overline{10}$ into $\overline{-10}\leq
I\leq\overline{10}$.

###  3.2 Completed definitions

Consider a regular program $\Pi$ and a predicate symbol $p/n$ that occurs in
$\Pi$. The _definition_ of $p/n$ in $\Pi$ is the set of all rules of $\Pi$
that have the form

$p({\bf t})\leftarrow\emph{Body\/}$ (5)

or

$\\{p({\bf t})\\}\leftarrow\emph{Body\/}$ (6)

such that the length of the tuple $\bf t$ is $n$. The _completed definition_
of $p/n$ in $\Pi$ is the sentence over $\sigma_{\Pi}$ constructed as follows.
Choose a tuple $\bf V$ of $n$ general variables that do not occur in $\Pi$.
For every rule $R$ in the definition $D$ of $p/n$ in $\Pi$, by $F_{R}$ we
denote the formula

$f_{R}(\emph{Body\/})\land{\bf V}=f_{R}({\bf t})$

if $R$ is (5), and

$f_{R}(\emph{Body\/})\land{\bf V}=f_{R}({\bf t})\land p({\bf V})$

if $R$ is (6). The completed definition of $p/n$ in $\Pi$ is the sentence

$\forall{\bf V}\left(p({\bf V})\leftrightarrow\bigvee_{R\in D}\exists{\bf
U}_{R}F_{R}\right),$ (7)

where ${\bf U}_{R}$ is the list of all variables occurring in
$f_{R}(\emph{Body\/})$ or in $f_{R}({\bf t})$.

For example, if the only rule $R$ of the program is (3), and $p/n$ is
$\emph{even\/}/1$, then $F_{R}$ is

$\overline{-10}\leq I\leq\overline{10}\,\land\,V=\overline{2}*I,$

where $I$ is $f_{R}(X)$. The completed definition of $\emph{even\/}/1$ is (2).

The formula obtained from the completed definition (7) by replacing the global
variables $\bf V$ with fresh integer variables will be called the _arithmetic
completed definition_ of $p/n$ in $\Pi$. For example, the arithmetic completed
definition of $\emph{even\/}/1$ in program (3) is

$\forall N(\emph{even\/}(N)\leftrightarrow\exists I(\overline{-10}\leq
I\leq\overline{10}\,\land\,N=\overline{2}*I)).$ (8)

The arithmetic completed definition is entailed by the completed definition,
but not the other way around. For example, from formula (2) we can derive
$\neg\emph{even\/}(t)$ for every symbolic constant $t$, but this conclusion is
not warranted by formula (8).

###  3.3 Natural completion

The _natural completion_ NCOMP$(\Pi)$ of a regular program $\Pi$ is the set of
sentences that includes

  * •

for every predicate symbol $p/n$ occurring in $\Pi$, its completed definition
in $\Pi$, and

  * •

for every constraint $\leftarrow\emph{Body\/}$ in $\Pi$, the universal closure
of the formula

$\neg f_{\leftarrow Body}(\emph{Body\/}).$

Consider, for example, the program that consists of rule (3), the choice rule

$\\{\emph{foo\/}(X)\\}\leftarrow\emph{even\/}(X)$ (9)

and the constraint

$\leftarrow\emph{not\/}\ \emph{foo\/}(\overline{0}).$ (10)

Its natural completion consists of the completed definition (2) of
$\emph{even\/}/2$, the completed definition of $\emph{foo\/}/1$

$\forall V(\emph{foo\/}(V)\leftrightarrow\exists X(\emph{even\/}(X)\land
X=V\land\emph{foo\/}(V))),$

which can be rewritten111When we talk about equivalent transformations of a
completed definition, equivalence is understood in the sense of classical
first-order logic. as

$\forall V(\emph{foo\/}(V)\to\emph{even\/}(V)),$

and the sentence $\neg\neg\emph{foo\/}(\overline{0})$, which is equivalent to
$\emph{foo\/}(\overline{0})$.

###  3.4 Relation to stable models

The _Herbrand base_ of a regular program $\Pi$ is the set of all regular atoms
$p(t_{1},\dots,t_{n})$ such that $p/n$ occurs in $\Pi$ and $t_{1},\dots,t_{n}$
are precomputed terms. If $S$ is a subset of the Herbrand base of $\Pi$ then
$S^{\uparrow}$ is the interpretation of the signature $\sigma_{\Pi}$ defined
as follows:

  * (i)

the universe of the sort _general_ in $S^{\uparrow}$ is the set of all
precomputed terms;

  * (ii)

the universe of the sort _integer_ in $S^{\uparrow}$ is the set of all
numerals;

  * (iii)

for every precomputed term $t$, $S^{\uparrow}(t)=t$;

  * (iv)

for every pair $m$, $n$ of integers,
$S^{\uparrow}(\overline{m}+\overline{n})=\overline{m+n}$, and similarly for
subtraction and multiplication;

  * (v)

for every pair $t_{1},~{}t_{2}$ of precomputed terms, $S^{\uparrow}$ satisfies
$t_{1}<t_{2}$ iff the relation $<$ holds for the pair $t_{1}$, $t_{2}$, and
similarly for the other comparison symbols.

###### Theorem 1

For any regular program $\Pi$ and any subset $S$ of its Herbrand base, if $S$
is a stable model of $\Pi$ then $S^{\uparrow}$ satisfies NCOMP$(\Pi)$.

The _positive predicate dependency graph_ of a regular program $\Pi$ is the
directed graph defined as follows. Its vertices are the predicate symbols
$p/n$ occurring in $\Pi$. It has an edge from $p/n$ to $q/m$ if $\Pi$ has a
rule (4) such that

  * •

_Head_ has the form $p(t_{1},\dots,t_{n})$ or $\\{p(t_{1},\dots,t_{n})\\}$,
and

  * •

one of the conjunctive terms of _Body_ has the form $q(t_{1},\dots,t_{m})$.

A regular program $\Pi$ is _tight_ if its positive predicate dependency graph
is acyclic.

For example, the positive predicate dependency graph of program (3), (9), (10)
has one edge, from $\emph{foo\/}/1$ to $\emph{even\/}/1$. This program is
tight.

###### Theorem 2

For any tight regular program $\Pi$ and any subset $S$ of its Herbrand base,
$S$ is a stable model of $\Pi$ iff $S^{\uparrow}$ satisfies NCOMP$(\Pi)$.

##  4 The puzzle

_Two mathematicians, S and P, talk about two integers, $M$ and $N$. S knows
the sum $M+N$, and P knows the product $M\times N$. Both S and P know also
that the integers are greater than 1; that their sum is not greater than 100;
and that $N$ is greater than $M$. The following conversation occurs:_

  1. 1.

_S says: P does not know_ $M$ and $N$.

  2. 2.

_P says: Now I know_ $M$ and $N$.

  3. 3.

_S says: Now I also know_ $M$ and $N$.

_What are $M$ and $N$? _

###  4.1 First-order axioms

Jayadev Misra’s approach to translating this puzzle into a first-order
language [Misra (2022), Section 2.8.3] involves the use of binary predicates
$b_{0},\dots,b_{3}$. The formula $b_{0}(M,N)$ expresses that before the
beginning of the conversation the pair $M$, $N$ was considered a possible
solution. This can be expressed by the formula

$b_{0}(M,N)\leftrightarrow 1<M<N\land M+N\leq 100.$ (11)

The formula $b_{1}(M,N)$ expresses that $M$, $N$ was considered a possible
solution at step 1, that is, after hearing the words “P does not know $M$ and
$N$”; and so forth.

There are several ways to write axioms for $b_{1}$, $b_{2}$ and $b_{3}$. One
possibility is described below.

We say that an integer $I$ is _puzzling at time 0_ if is there is more than
one way to represent it as the product of two numbers $J$, $K$ satisfying
$b_{0}(J,K)$:

$\begin{array}[]{r}\\!\\!\emph{puzzling\/}_{0}(I)\leftrightarrow\exists
J_{1}K_{1}J_{2}K_{2}(b_{0}(J_{1},K_{1})\land b_{0}(J_{2},K_{2})\hskip
64.01869pt\\\ \land\,I=J_{1}\times K_{1}=J_{2}\times K_{2}\land J_{1}\neq
J_{2}).\end{array}$ (12)

We say that an integer $I$ is _possibly easy_ if it can be represented as the
sum of two numbers $J$, $K$ satisfying $b_{0}(J,K)$ such that $J\times K$ is
not puzzling at time 0:

$\emph{possibly\\_easy\/}(I)\leftrightarrow\exists JK(b_{0}(J,K)\land
I=J+K\land\neg\emph{puzzling\/}_{0}(J\times K)).$ (13)

Then the assumption

“at Step 1, S knows that P does not know $M$ and $N$”

can be expressed by the axiom

$b_{1}(M,N)\leftrightarrow b_{0}(M,N)\land\neg\emph{possibly\\_easy\/}(M+N).$
(14)

We say that an integer $I$ is _puzzling at time 1_ is there is more than one
way to represent it as the product of two numbers $J$, $K$ satisfying
$b_{1}(J,K)$:

$\begin{array}[]{r}\\!\\!\emph{puzzling\/}_{1}(I)\leftrightarrow\exists
J_{1}K_{1}J_{2}K_{2}(b_{1}(J_{1},K_{1})\land b_{1}(J_{2},K_{2})\hskip
64.01869pt\\\ \land\,I=J_{1}\times K_{1}=J_{2}\times K_{2}\land J_{1}\neq
J_{2}).\end{array}$ (15)

The assumption

“at Step 2, P knows $M$ and $N$”

can be expressed by the axiom

$b_{2}(M,N)\leftrightarrow b_{1}(M,N)\land\neg\emph{puzzling\/}_{1}(M\times
N).$ (16)

We say that an integer $I$ is _puzzling at time 2_ is there is more than one
way to represent it as the sum of two numbers $J$, $K$ satisfying
$b_{2}(J,K)$:

$\begin{array}[]{r}\\!\\!\emph{puzzling\/}_{2}(I)\leftrightarrow\exists
J_{1}K_{1}J_{2}K_{2}(b_{2}(J_{1},K_{1})\land b_{2}(J_{2},K_{2})\hskip
64.01869pt\\\ \land\,I=J_{1}+K_{1}=J_{2}+K_{2}\land J_{1}\neq
J_{2}).\end{array}$ (17)

Finally, the assumption

“at Step 3, S knows $M$ and $N$”

can be expressed by the axiom

$b_{3}(M,N)\leftrightarrow b_{2}(M,N)\land\neg\emph{puzzling\/}_{2}(M+N).$
(18)

Since axioms (11)–(18) form a chain of explicit definitions, the predicates
represented by the symbols

$b_{0}/2,\ \dots,\ b_{3}/2,\ \emph{puzzling\/}_{0}/1,\ \dots,\
\emph{puzzling\/}_{2}/1,\ \emph{possibly\\_easy\/}/1$ (19)

are uniquely defined, assuming that variables range over the integers and that
the symbols

$+\quad\times\quad<\quad\leq$

are interpreted in the standard way. To solve the Sum and Product Puzzle, we
will calculate the extents of these predicates.

This will be accomplished by running clingo on the “reverse completion” of
axioms (11)–(18).

###  4.2 Reverse completion

Consider the regular program

$\begin{array}[]{rcl}b_{0}(\emph{XM\/},\emph{XN\/})&\leftarrow&\overline{1}<\emph{XM\/}\,\land\,\emph{XM\/}<\emph{XN\/}\,\land\,\emph{XM\/}+\emph{XN\/}\leq\overline{100},\\\
\emph{puzzling\/}_{0}(\emph{XI})&\leftarrow&b_{0}(\emph{XJ}_{1},\emph{XK}_{1})\,\land\,b_{0}(\emph{XJ}_{2},\emph{XK}_{2})\,\land\,\emph{XI}=\emph{XJ}_{1}\times\emph{XK}_{1}\\\
&&\hskip
28.45274pt\land\;\emph{XJ}_{1}\times\emph{XK}_{1}=\emph{XJ}_{2}\times\emph{XK}_{2}\,\land\,\emph{XJ}_{1}\neq\emph{XJ}_{2},\\\
\emph{possibly\\_easy\/}(\emph{XI})&\leftarrow&b_{0}(\emph{XJ},\emph{XK})\,\land\,\emph{XI}=\emph{XJ}+\emph{XK}\\\
&&\land\;\emph{not\/}\ \emph{puzzling\/}_{0}(\emph{XJ}\times\emph{XK}),\\\
b_{1}(\emph{XM\/},\emph{XN\/})&\leftarrow&b_{0}(\emph{XM\/},\emph{XN\/})\,\land\,\emph{not\/}\
\emph{possibly\\_easy\/}(\emph{XM\/}+\emph{XN\/}),\\\
\emph{puzzling\/}_{1}(\emph{XI})&\leftarrow&b_{1}(\emph{XJ}_{1},\emph{XK}_{1})\,\land\,b_{1}(\emph{XJ}_{2},\emph{XK}_{2})\,\land\,\emph{XI}=\emph{XJ}_{1}\times\emph{XK}_{1}\\\
&&\hskip
28.45274pt\land\;\emph{XJ}_{1}\times\emph{XK}_{1}=\emph{XJ}_{2}\times\emph{XK}_{2}\,\land\,\emph{XJ}_{1}\neq\emph{XJ}_{2},\\\
b_{2}(\emph{XM\/},\emph{XN\/})&\leftarrow&b_{1}(\emph{XM\/},\emph{XN\/})\,\land\,\emph{not\/}\
\emph{puzzling\/}_{1}(\emph{XM\/}\times\emph{XN\/}),\\\
\emph{puzzling\/}_{2}(\emph{XI})&\leftarrow&b_{2}(\emph{XJ}_{1},\emph{XK}_{1})\,\land\,b_{2}(\emph{XJ}_{2},\emph{XK}_{2})\,\land\,\emph{XI}=\emph{XJ}_{1}+\emph{XK}_{1}\\\
&&\hskip
28.45274pt\land\;\emph{XJ}_{1}+\emph{XK}_{1}=\emph{XJ}_{2}+\emph{XK}_{2}\,\land\,\
\emph{XJ}_{1}\neq\emph{XJ}_{2},\\\
b_{3}(\emph{XM\/},\emph{XN\/})&\leftarrow&b_{2}(\emph{XM\/},\emph{XN\/})\,\land\,\emph{not\/}\
\emph{puzzling\/}_{2}(\emph{XM\/}+\emph{XN\/}).\end{array}$ (20)

These rules are obtained from equivalences (11)–(18) by

  * •

replacing the equivalence signs $\leftrightarrow$ by left arrows,

  * •

dropping existential quantifiers,

  * •

replacing integer variables by general variables, and

  * •

replacing $\neg$ by _not_.

The natural completion of program (20) looks very similar to axiom set
(11)–(18). There is a difference though: the former consists of formulas over
the two-sorted signature described in Section 2.2, and the axioms formalizing
the Sum and Product puzzle are one-sorted; there are no general variables in
them. Consider then the _arithmetic_ completed definitions of predicate
symbols (19) (see Section 3.2). Those are one-sorted formulas, and they are
equivalent to the universal closures of the corresponding axioms. For example,
the completed definition of the predicate symbol $b_{0}/2$ in program (20) is

$\begin{array}[]{l}\forall\emph{XM\/}\,\emph{XN\/}(b_{0}(\emph{XM\/},\emph{XN\/})\leftrightarrow\\\
\hskip 51.21504pt\exists MN(\overline{1}<M\land M<N\land
M+N\leq\overline{100}\land\emph{XM\/}=M\land\emph{XN\/}=N)),\end{array}$

and the arithmetic completed definition of this symbol is the one-sorted
formula

$\begin{array}[]{l}\forall M_{1}N_{1}(b_{0}(M_{1},N_{1})\leftrightarrow\\\
\hskip 51.21504pt\exists MN(\overline{1}<M\land M<N\land
M+N\leq\overline{100}\land M_{1}=M\land N_{1}=N)).\end{array}$

This formula is equivalent to the universal closure of axiom (11). Similarly,
the arithmetic completed definition of $\emph{puzzling\/}_{0}/2$ is equivalent
to the universal closure of axiom (12), and so forth.

###  4.3 Calculating the answer

By running clingo we can determine that program (20) has a unique stable model
$S$. By Theorem 1, the interpretation $S^{\uparrow}$ satisfies the completed
definitions of symbols (19). It follows that $S^{\uparrow}$ satisfies the
arithmetic completed definitions of these symbols, which are equivalent to
axioms (11)–(18). In other words, $S$ describes the extents of the predicates
that we want to calculate. Since the only atom in $S$ that begins with $b_{3}$
is $b_{3}(\overline{4},\overline{13})$, the answer to the puzzle is

$M=4,\ N=13.$

To perform this calculation, we used version 5.6.0 of clingo. Earlier versions
do not accept the first rule of the program as safe unless the expression

$\overline{1}<M\land M<N$

in the body is rewritten in the interval notation:
$M=\overline{2}\,..\,N-\overline{1}$.

##  5 Proofs

Proofs of Theorems 1 and 2 are based on similar results from an earlier
publication [Fandinno et al. (2020)], and we begin by reviewing them for the
special case of regular programs.

###  5.1 Review: Completion according to Fandinno et al.

For any regular term $t$, the formula $\emph{val\,}_{t}({Z})$, where $Z$ is a
general variable that does not occur in $t$, is defined recursively:

  * •

if $t$ is a numeral or a variable then $\emph{val\,}_{t}({Z})$ is $Z=t$;

  * •

if $t$ is $t_{1}+t_{2}$ then $\emph{val\,}_{t}({Z})$ is

$\exists
IJ(Z=I+J\land\emph{val\,}_{t_{1}}({I})\land\emph{val\,}_{t_{2}}({J})),$

and similarly for $t_{1}-t_{2}$ and $t_{1}\times t_{2}$.

If $t$ is a symbolic constant then $\emph{val\,}_{t}({Z})$ stands for $Z=t$.
If $t_{1},\dots,t_{k}$ is a tuple of symbolic constants and regular terms, and
$Z_{1},\dots,Z_{k}$ are pairwise distinct general variables that do not occur
in $t_{1},\dots,t_{k}$, then
$\emph{val\,}_{t_{1},\dots,t_{k}}({Z_{1},\dots,Z_{k}})$ stands for
$\emph{val\,}_{t_{1}}({Z_{1}})\land\cdots\land\emph{val\,}_{t_{k}}({Z_{k}})$.
If $t$ is $t_{1}\,..\,t_{2}$ then $\emph{val\,}_{t}({Z})$ stands for

$\exists IJK(\emph{val\,}_{t_{1}}({I})\land\emph{val\,}_{t_{2}}({J})\land
I\leq K\leq J\land Z=K).$

The translation $\tau^{B}$ transforms expressions in the body of a regular
rule into formulas as follows:

  * •

$\tau^{B}(p({\bf t}))$ is $\exists{\bf Z}(\emph{val\,}_{\bf t}({\bf Z})\land
p({\bf Z}))$, where $\bf Z$ is a tuple of distinct program variables that do
not occur in $\bf t$;

  * •

$\tau^{B}(\emph{not\/}\ p({\bf t}))$ is $\exists{\bf
Z}(\emph{val\,}_{\bf{}_{t}}({\bf Z})\land\neg p({\bf Z}))$;

  * •

$\tau^{B}(t_{1}\prec t_{2})$ is $\exists
Z_{1}Z_{2}(\emph{val\,}_{t_{1},t_{2}}({Z_{1},Z_{2}})\land Z_{1}\prec Z_{2})$;

  * •

$\tau^{B}(t_{1}=t_{2}\,..\,t_{3})$ is $\exists
Z_{1}Z_{2}(\emph{val\,}_{t_{1}}({Z_{1}})\land\emph{val\,}_{t_{2}\,..\,t_{3}}({Z_{2}})\land
Z_{1}=Z_{2})$;

  * •

$\tau^{B}(B_{1}\land B_{2}\land\cdots)$ is
$\tau^{B}(B_{1})\land\tau^{B}(B_{2})\land\cdots$.

The _completed definition of $p/n$ in $\Pi$ in the sense of Fandinno et al._
is the sentence over $\sigma_{\Pi}$ constructed as follows. Choose a tuple
$\bf V$ of $n$ general variables that do not occur in $\Pi$. For every rule
$R$ in the definition $D$ of $p/n$ in $\Pi$, by $F^{\prime}_{R}$ we denote the
formula

$\tau^{B}(\emph{Body\/})\land\emph{val\,}_{\bf t}({\bf V})$

if $R$ is (5), and

$\tau^{B}(\emph{Body\/})\land\emph{val\,}_{\bf t}({\bf V})\land p({\bf V})$

if $R$ is (6). The completed definition of $p/n$ in $\Pi$ according to
Fandinno _et al._ is the sentence

$\forall{\bf V}\left(p({\bf V})\leftrightarrow\bigvee_{R\in D}\exists{\bf
U}^{\prime}_{R}F^{\prime}_{R}\right),$

where ${\bf U}^{\prime}_{R}$ is the list of all variables occurring in $R$.

For example, the completed definition of one-rule program (3) is

$\forall V\left(\emph{even\/}(V)\leftrightarrow\exists X\left(\exists
Z_{1}Z_{2}\left(Z_{1}=X\land\emph{val\,}_{\overline{-10}\,..\,\overline{10}}({Z_{2}})\land
Z_{1}=Z_{2}\right)\land\emph{val\,}_{\overline{2}\times
X}({V})\right)\right),$ (21)

where $\emph{val\,}_{\overline{-10}\,..\,\overline{10}}({Z_{2}})$ stands for

$\exists IJK(I=\overline{-10}\land J=\overline{10}\land I\leq K\leq J\land
Z_{2}=K)$

and $\emph{val\,}_{\overline{2}\times X}({V})$ stands for

$\exists IJ(V=I\times J\land I=\overline{2}\land J=X).$

By COMP$(\Pi)$ we denote the set of sentences that includes

  * •

for every predicate symbol $p/n$ occurring in $\Pi$, its completed definition
in $\Pi$ in the sense of Fandinno et al, and

  * •

for every constraint $\leftarrow\emph{Body\/}$ in $\Pi$, the universal closure
of the formula $\neg\tau^{B}(\emph{Body\/})$.

###### Lemma 1

For any regular program $\Pi$ and any subset $S$ of its Herbrand base, if $S$
is a stable model of $\Pi$ then $S^{\uparrow}$ satisfies COMP$(\Pi)$ [Fandinno
et al. (2020), Theorem 1].

###### Lemma 2

For any tight regular program $\Pi$ and any subset $S$ of its Herbrand base,
$S$ is a stable model of $\Pi$ iff $S^{\uparrow}$ satisfies COMP$(\Pi)$
[Fandinno et al. (2020), Theorem 2].

###  5.2 Main Lemma

Theorems 1 and 2 follow from Lemmas 1 and 2 in view of the following fact,
proved below:

_Main Lemma_
For any regular program $\Pi$, the formula NCOMP$(\Pi)$ is equivalent to
COMP$(\Pi)$ in classical predicate calculus with equality.

In the statements of Lemmas 3–7, $R$ is a regular rule, $\bf X$ is the list of
its critical variables, and $\bf I$ is $f_{R}({\bf X})$.

###### Lemma 3

If $\bf t$ is a list of symbolic constants and regular terms that occur in
$R$, and $\bf Z$ is a list of pairwise distinct general variables that do not
occur in $R$, then the formula

${\bf I}={\bf X}\to\forall{\bf Z}(val_{\bf t}({\bf Z})\leftrightarrow{\bf
Z}=f_{R}({\bf t}))$ (22)

is logically valid [Lifschitz (2021), Lemma 1(i)].

###### Lemma 4

For any regular atom $p({\bf t})$ occurring in $R$, the formulas

$\begin{array}[]{l}{\bf I}={\bf X}\to(f_{R}(p({\bf
t}))\leftrightarrow\tau^{B}(p({\bf t}))),\\\ {\bf I}={\bf X}\to(f_{R}(not\
p({\bf t}))\leftrightarrow\tau^{B}(not\ p({\bf t})))\end{array}$

are logically valid [Lifschitz (2021), Lemma 1(iii,iv)].

###### Lemma 5

For any comparison $t_{1}\prec t_{2}$ occurring in $R$, the formula

${\bf I}={\bf X}\to(f_{R}(t_{1}\prec t_{2})\leftrightarrow\tau^{B}(t_{1}\prec
t_{2}))$

is logically valid [Lifschitz (2021), Lemma 2].

###### Lemma 6

For any comparison $t_{1}=t_{2}\,..\,t_{3}$ occurring in $R$, the formula

${\bf I}={\bf
X}\to(f_{R}(t_{1}=t_{2}\,..\,t_{3})\leftrightarrow\tau^{B}(t_{1}=t_{2}\,..\,t_{3}))$

is logically valid [Lifschitz (2021), Lemma 4].

From Lemmas 4–6 we conclude:

###### Lemma 7

The formula

${\bf I}={\bf X}\to(f_{R}(Body)\leftrightarrow\tau^{B}(Body)),$ (23)

where _Body_ is the body of $R$, is logically valid.

###### Lemma 8

Let $R$ be a regular rule with the body $B_{1}\land B_{2}\land\cdots$.

  * (a)

For every variable $X$ that occurs in $B_{i}$ in the scope of an arithmetic
operation, the formula

$\tau^{B}(B_{i})\to\exists I(I=X)$ (24)

is logically valid.

  * (b)

If $B_{i}$ is a comparison of the form $t_{1}=t_{2}\,..\,t_{3}$ then formula
(24) is logically valid for every variable $X$ that occurs in $B_{i}$.

[Lifschitz (2021), Lemmas 7 and 9].

From Lemma 8 we conclude:

###### Lemma 9

Let $R$ be a regular rule, and let $\bf X$ be the list of its critical
variables. The formula

$\tau^{B}(Body)\to\exists{\bf I}({\bf I}={\bf X}),$ (25)

where _Body_ is the body of $R$ and $\bf I$ is $f_{R}({\bf X})$, is logically
valid.

In the following lemma, $R$ is a regular rule of form (5) or (6), $F_{R}$ and
${\bf U}_{R}$ are as defined in Section 3.2, and $F^{\prime}_{R}$ and ${\bf
U}^{\prime}_{R}$ are as defined in Section 5.1.

###### Lemma 10

The formula $\exists{\bf U}^{\prime}_{R}F^{\prime}_{R}$ is equivalent to
$\exists{\bf U}_{R}F_{R}$.

Proof  Let $\bf X$ be the list of all critical variables of $R$, and let $\bf
I$ be $f_{R}({\bf X})$. It is sufficient to prove the equivalence

$\exists{\bf I}\,F^{\prime}_{R}\leftrightarrow\exists{\bf X}\,F_{R}.$

We consider the case when $R$ is (5), so that $F_{R}$ is

$\tau^{B}(\emph{Body\/})\land\emph{val\,}_{\bf t}({\bf V})$

and $F^{\prime}_{R}$ is

$f_{R}(\emph{Body\/})\land{\bf V}=f_{R}({\bf t}).$

The case of rule (6) is similar.

Left-to-right: assume $\exists{\bf I}(f_{R}(\emph{Body\/})\land{\bf
V}=f_{R}({\bf t}))$. Since $\forall{\bf I}\exists{\bf X}({\bf I}={\bf X})$, we
can conclude that

$\exists{\bf I}(\exists{\bf X}({\bf I}={\bf X})\land
f_{R}(\emph{Body\/})\land{\bf V}=f_{R}({\bf t})).$

It follows that

$\exists{\bf IX}({\bf I}={\bf X}\land f_{R}(\emph{Body\/})\land{\bf
V}=f_{R}({\bf t})),$

because the critical variables $\bf X$ do not occur in the formula
$f_{R}(\emph{Body\/})\land{\bf V}=f_{R}({\bf t})$. Then $\exists{\bf
IX}(\tau^{B}(\emph{Body\/})\land\emph{val\,}_{\bf t}({\bf V}))$ follows using
the iniversal closures of (22) and (23). Since the integer variables $\bf I$
do not occur in $\tau^{B}(\emph{Body\/})\land\emph{val\,}_{\bf t}({\bf V})$,
the quantifiers binding $\bf I$ can be dropped.

Right-to-left: assume $\exists{\bf
X}(\tau^{B}(\emph{Body\/})\land\emph{val\,}_{\bf t}({\bf V}))$. We can
conclude, using the universal closure of (25), that

$\exists{\bf X}(\exists{\bf I}({\bf I}={\bf
X})\land\tau^{B}(\emph{Body\/})\land\emph{val\,}_{\bf t}({\bf V})).$

It follows that

$\exists{\bf IX}({\bf I}={\bf
X}\land\tau^{B}(\emph{Body\/})\land\emph{val\,}_{\bf t}({\bf V})),$

because the integer variables $\bf I$ do not occur in the formula
$\tau^{B}(\emph{Body\/})\land\emph{val\,}_{\bf t}({\bf V}))$. Then
$\exists{\bf IX}(f_{R}(\emph{Body\/})\land{\bf V}=f_{R}({\bf t}))$ follows
using the iniversal closures of (22) and (23). Since the critical variables
$\bf X$ do not occur in $f_{R}(\emph{Body\/})\land{\bf V}=f_{R}({\bf t})$, the
quantifiers binding $\bf X$ can be dropped.

###### Lemma 11

If $R$ is a regular constraint $\leftarrow Body$ then the universal closures
of the formulas $\neg f_{R}(Body)$ and $\neg\tau^{B}(Body)$ are equivalent to
each other.

Proof  Let $\bf X$ be the list of all critical variables of $R$, and let $\bf
I$ be $f_{R}({\bf X})$. It is sufficient to prove the equivalence

$\exists{\bf I}\,f_{R}(\emph{Body\/})\leftrightarrow\exists{\bf
X}\,\tau^{B}(\emph{Body\/}),$

because it entails

$\forall{\bf I}\neg f_{R}(\emph{Body\/})\leftrightarrow\forall{\bf
X}\neg\tau^{B}(\emph{Body\/})$

and consequently entails also the equivalence between the universal closures
of $\neg f_{R}(Body)$ and $\neg\tau^{B}(Body)$.

Left-to-right: assume $\exists{\bf I}\,f_{R}(\emph{Body\/})$. Since
$\forall{\bf I}\exists{\bf X}({\bf I}={\bf X})$, we can conclude that

$\exists{\bf IX}({\bf I}={\bf X}\land f_{R}(\emph{Body\/})),$

because the critical variables $\bf X$ do not occur in $f_{R}(\emph{Body\/})$.
Then $\exists{\bf IX}\,\tau^{B}(\emph{Body\/})$ follows using the iniversal
closure of (23). Since the integer variables $\bf I$ do not occur in
$\tau^{B}(\emph{Body\/})$, the quantifiers binding $\bf I$ can be dropped.

Right-to-left: assume $\exists{\bf X}\,\tau^{B}(\emph{Body\/})$. We can
conclude, using the universal closure of (25), that

$\exists{\bf IX}({\bf I}={\bf X}\land\tau^{B}(\emph{Body\/})),$

because the integer variables $\bf I$ do not occur in
$\tau^{B}(\emph{Body\/})$. Then $\exists{\bf IX}\,f_{R}(\emph{Body\/})$
follows using the iniversal closure of (23). Since the critical variables $\bf
X$ do not occur in $f_{R}(\emph{Body\/})$, the quantifiers binding $\bf X$ can
be dropped.

Main Lemma follows from Lemmas 10 and 11.

##  6 Discussion

In the presence of arithmetic operations, the completed definition in the
sense of Fandinno et al. is often longer and syntactically more complex than
the “natural” completed definition introduced in Section 3.2; compare, for
instance, formula (21) with (2). On the other hand, the approach of Fandinno
et al. is applicable to some types of rules that are accepted by clingo but
are not regular, such as

      p(1..8,1..8).
      p(2*(1..8)).

These two rules can be easily rewritten as regular rules:

      p(X,Y) :- X = 1..8, Y = 1..8.
      p(2*X) :- X = 1..8.

Regularizing the rule

      q(X/5) :- p(X).

in a similar way gives the rule

      q(Y) :- p(X), X = 5*Y+Z, Z = 0..4.

that the current version of clingo considers unsafe.

The translation COMP is used in the design of the proof assistant anthem
[Fandinno et al. (2020)], and our Main Lemma shows that NCOMP can be employed
in the same way. In the process of interacting with anthem, the user often has
to read and modify completion formulas. A version of anthem that implements
natural completion would make this work easier.

It would be interesting to extend the definition of NCOMP to programs
containing conditional literals [Gebser et al. (2019), Section 3.1.11]. Such
an extension would make the reverse completion process applicable to some
formulas that are more complex syntactically than the current version. For
instance, it may be able to handle the formula

$\begin{array}[]{l}b_{1}(M,N)\,\leftrightarrow\\\ \qquad
b_{0}(M,N)\land\neg\exists JK(b_{0}(J,K)\land
M+N=J+K\land\neg\emph{puzzling\/}_{0}(J\times K)),\end{array}$

which can replace axioms (13), (14) in the first-order formalization of the
Sum and Product Puzzle.

## Acknowledgements

Many thanks to Jorge Fandinno, Michael Gelfond, Yuliya Lierler, Jayadev Misra
and Nathan Temple for discussions related to the topic of this paper, and to
the anonymous referees for advice on improving the previous version.

## References

  * Calimeri et al. (2020) Calimeri, F., Faber, W., Gebser, M., Ianni, G., Kaminski, R., Krennwallner, T., Leone, N., Maratea, M., Ricca, F., and Schaub, T. 2020\.  ASP-Core-2 input language format.  Theory and Practice of Logic Programming 20, 294–309.
  * Clark (1978) Clark, K. 1978\.  Negation as failure.  In Logic and Data Bases, H. Gallaire and J. Minker, Eds. Plenum Press, New York, 293–322.
  * Fages (1991) Fages, F. 1991\.  A fixpoint semantics for general logic programs compared with the well-supported and stable model semantics.  New Generation Computing 9, 425–443.
  * Fandinno et al. (2020) Fandinno, J., Lifschitz, V., Lühne, P., and Schaub, T. 2020\.  Verifying tight logic programs with Anthem and Vampire.  Theory and Practice of Logic Programming 20.
  * Gebser et al. (2015) Gebser, M., Harrison, A., Kaminski, R., Lifschitz, V., and Schaub, T. 2015\.  Abstract Gringo.  Theory and Practice of Logic Programming 15, 449–463.
  * Gebser et al. (2019) Gebser, M., Kaminski, R., Kaufmann, B., Lindauer, M., Ostrowski, M., Romero, J., Schaub, T., and Thiele, S. 2019\.  Potassco User Guide.  Available at https://github.com/potassco/guide/releases/.
  * Lierler and Maratea (2004) Lierler, Y. and Maratea, M. 2004\.  Cmodels-2: SAT-based answer set solver enhanced to non-tight programs.  In Procedings of International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR). 346–350.
  * Lifschitz (2021) Lifschitz, V. 2021\.  Transforming gringo rules into formulas in a natural way.  In Proceedings of European Conference on Artificial Intelligence.
  * Lifschitz et al. (2019) Lifschitz, V., Lühne, P., and Schaub, T. 2019\.  Verifying strong equivalence of programs in the input language of gringo.  In Proceedings of the 15th International Conference on Logic Programming and Non-monotonic Reasoning.
  * Lin and Zhao (2004) Lin, F. and Zhao, Y. 2004\.  ASSAT: Computing answer sets of a logic program by SAT solvers.  Artificial Intelligence 157, 115–137.
  * Lloyd and Topor (1984) Lloyd, J. and Topor, R. 1984\.  Making Prolog more expressive.  Journal of Logic Programming 1, 225–240.
  * McCarthy (1990) McCarthy, J. 1990\.  Formalization of two puzzles involving knowledge.  In Formalizing Common Sense: Papers by John McCarthy. Ablex, Norwood, NJ.
  * Misra (2022) Misra, J. 2022\.  Effective Theories in Programming Practice.  Association for Computing Machinery.
  * van Ditmarsch et al. (2005) van Ditmarsch, H., Ruan, J., and Verbrugge, L. C. 2005\.  Model checking sum and product.  In Proceedings of Australasian Joint Conference on Artificial Intelligence. 790–795.