In deductive systems including a single negation operator , any formula that is either atomic or the negation of an atomic formula. For example, in a propositional language in which atoms are of the form where is a sentence letter, the literals are the collection of formulae of the form or .