  The formal XAI community has studied a plethora of interpretability queries
aiming to understand the classifications made by decision trees. However, a
more uniform understanding of what questions we can hope to answer about these
models, traditionally deemed to be easily interpretable, has remained elusive.
In an initial attempt to understand uniform languages for interpretability,
Arenas et al. (2021) proposed FOIL, a logic for explaining black-box ML models,
and showed that it can express a variety of interpretability queries. However,
we show that FOIL is limited in two important senses: (i) it is not expressive
enough to capture some crucial queries, and (ii) its model agnostic nature
results in a high computational complexity for decision trees. In this paper,
we carefully craft two fragments of first-order logic that allow for
efficiently interpreting decision trees: Q-DT-FOIL and its optimization variant
OPT-DT-FOIL. We show that our proposed logics can express not only a variety of
interpretability queries considered by previous literature, but also elegantly
allows users to specify different objectives the sought explanations should
optimize for. Using finite model-theoretic techniques, we show that the
different ingredients of Q-DT-FOIL are necessary for its expressiveness, and
yet that queries in Q-DT-FOIL can be evaluated with a polynomial number of
queries to a SAT solver, as well as their optimization versions in OPT-DT-FOIL.
Besides our theoretical results, we provide a SAT-based implementation of the
evaluation for OPT-DT-FOIL that is performant on industry-size decision trees.
