Answer:
In mathematical logic, a literal is an atomic formula (atom) or its negation. The definition mostly appears in proof theory (of classical logic), e.g. in conjunctive normal form and the method of resolution.
Literals can be divided into two types:
A positive literal is just an atom (e.g., {\displaystyle x}x).
A negative literal is the negation of an atom (e.g., {\displaystyle \lnot x}\lnot x).
The polarity of a literal is positive or negative depending on whether it is a positive or negative literal.
For a literal {\displaystyle l}l, the complementary literal is a literal corresponding to the negation of {\displaystyle l}l, we can write {\displaystyle {\bar {l}}}{\bar {l}} to denote the complementary literal of {\displaystyle l}l.
More precisely, if {\displaystyle l\equiv x}l\equiv x then {\displaystyle {\bar {l}}}{\bar {l}} is {\displaystyle \lnot x}\lnot x and if {\displaystyle l\equiv \lnot x}l\equiv \lnot x then {\displaystyle {\bar {l}}}{\bar {l}} is {\displaystyle x}x.
In the context of a formula in the conjunctive normal form, a literal is pure if the literal's complement does not appear in the formula.
In Boolean functions, each separate occurrence of a variable, either in inverse or uncomplemented form, is a literal. For example, if {\displaystyle A}A, {\displaystyle B}B and {\displaystyle C}C are variables then the expression {\displaystyle {\bar {A}}BC}{\displaystyle {\bar {A}}BC} contains three literals and the expression {\displaystyle {\bar {A}}C+{\bar {B}}{\bar {C}}}{\displaystyle {\bar {A}}C+{\bar {B}}{\bar {C}}} contains four literals. However, the expression {\displaystyle {\bar {A}}C+{\bar {B}}C}{\displaystyle {\bar {A}}C+{\bar {B}}C} would also be said to contain four literals, because although two of the literals are identical ({\displaystyle C}C appears twice) these qualify as two separate occurrences.
