Symmetry

Given that the pigeonhole problem and clique-coloring problems involve a great deal of symmetry in their arguments, a variety of authors have suggested extending Boolean representation or inference in a way that allows this symmetry to be exploited directly. We will discuss the variety of approaches that have been proposed by separating them based on whether or not a modification to the basic resolution inference rule is suggested. In any event, we make the following definition:

As an example, if consists of the single axiom , then
is clearly symmetric under the exchange of and . If
contains the two axioms

and

then is once again symmetric under the exchange of and .