Recent years have witnessed a renewed interest in Boolean function in explaining binary classifiers in the field of explainable AI (XAI). The standard approach of Boolean function is propositional logic. We present a modal language of a ceteris paribus nature which supports reasoning about binary input classifiers and their properties. We study a family of classifier models, axiomatize it as two proof systems regarding the cardinality of the language and show completeness of our axiomatics. Moreover, we prove that satisfiability checking problem for our modal language is NEXPTIME-complete in the infinite-variable case, while it becomes polynomial in the finite-variable case. We furthermore identify an interesting NP fragment of our language in the infinite-variable case. We leverage the language to formalize counterfactual conditional as well as a variety of notions of explanation including abductive, contrastive and counterfactual explanations, and biases. Finally, we present two extensions of our language: a dynamic extension by the notion of assignment enabling classifier change and an epistemic extension in which the classifier's uncertainty about the actual input can be represented.

翻译：近年来，可解释人工智能（XAI）领域中对布尔函数在解释二元分类器方面的研究重新引起了关注。布尔函数的标准方法基于命题逻辑。我们提出了一种具有“其他条件相同”性质的模态语言，该语言支持对二元输入分类器及其属性进行推理。我们研究了一族分类器模型，根据语言的基数将其公理化地构建为两个证明系统，并展示了我们公理系统的完备性。此外，我们证明了在我们模态语言中，无限变量情况下的可满足性判定问题是NEXPTIME完全的，而在有限变量情况下则变为多项式时间可解。在无限变量情况下，我们还识别出一个有趣的NP片段。我们利用该语言形式化了反事实条件以及多种解释概念，包括溯因解释、对比解释、反事实解释和偏见。最后，我们提出了该语言的两种扩展：一种是通过赋值概念实现分类器变更的动态扩展，另一种是能够表示分类器对实际输入不确定性的认知扩展。