On Quantifying Literals in Boolean Logic and its Applications to Explainable AI (Extended Abstract)

Abstract

Quantified Boolean logic results from adding operators to Boolean logic for existentially and universally quantifying variables. This extends the reach of Boolean logic by enabling a variety of applications that have been explored over the decades. The existential quantification of literals (variable states) and its applications have also been studied in the literature. We complement this by studying universal literal quantification and its applications, particularly to explainable AI. We also provide a novel semantics for quantification and discuss the interplay between variable/literal and existential/universal quantification. We further identify classes of Boolean formulas and circuits that allow efficient quantification. Literal quantification is more fine-grained than variable quantification, which leads to a refinement of quantified Boolean logic with literal quantification as its primitive.