  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. In this paper,
we complement this by studying universal literal quantification and its
applications, particularly to explainable AI. We also provide a novel semantics
for quantification, discuss the interplay between variable/literal and
existential/universal quantification. We further identify some classes of
Boolean formulas and circuits on which quantification can be done efficiently.
Literal quantification is more fine-grained than variable quantification as the
latter can be defined in terms of the former. This leads to a refinement of
quantified Boolean logic with literal quantification as its primitive.
