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.