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片段。我们利用该语言形式化了反事实条件句以及多种解释概念，包括溯因解释、对比解释、反事实解释和偏差。最后，我们提出了该语言的两种扩展：一种是通过赋值概念实现的动态扩展，支持分类器变更；另一种是认知扩展，能够表示分类器对实际输入的不确定性。