In mathematical logic, a literal is an atomic formula or its negation. The definition mostly appears in proof theory , e.g. in conjunctive normal form and the method of resolution.
Literals can be divided into two types:
The polarity of a literal is positive or negative depending on whether it is a positive or negative literal.
For a literal l {\displaystyle l} , the complementary literal is a literal corresponding to the negation of l {\displaystyle l} , we can write l ¯ {\displaystyle {\bar {l}}} to denote the complementary literal of l {\displaystyle l}. More precisely, if l ≡ x {\displaystyle l\equiv x} then l ¯ {\displaystyle {\bar {l}}} is ¬ x {\displaystyle \lnot x} and if l ≡ ¬ x {\displaystyle l\equiv \lnot x} then l ¯ {\displaystyle {\bar {l}}} is x {\displaystyle x}.