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）领域中，布尔函数在解释二分类器方面重新引起了研究兴趣。布尔函数的标准方法是命题逻辑。我们提出了一种基于"其余条件相同"（ceteris paribus）性质的模态语言，该语言支持对二值输入分类器及其属性的推理。我们研究了一族分类器模型，根据语言基数的不同将其公理化地构建为两个证明系统，并证明了我们公理系统的完备性。此外，我们证明：在无限变量情况下，该模态语言的可满足性判定问题为NEXPTIME完全问题，而在有限变量情况下则变为多项式时间问题。在无限变量情况下，我们还识别出一个有趣的NP片段。我们利用该语言形式化了反事实条件句，以及多种解释概念，包括溯因解释、对比解释、反事实解释和偏差。最后，我们提出了该语言的两种扩展：一种是通过赋值概念实现的动态扩展，使得分类器能够发生变化；另一种是认知扩展，可以表示分类器对实际输入的不确定性。