Let be a signature and the set of terms over . The set of symbols for is the disjoint union of and , a countably infinite set whose elements are called variables. Now, adjoin the set , assumed to be disjoint from . An atomic formula over is any one of the following:

1. either , where and are terms in ,
2. or , where is an -ary relation symbol, and .

Remarks.

1. Using atomic formulas, one can inductively build formulas using the logical connectives , , , etc... In this sense, atomic formulas are formulas that can not be broken down into simpler formulas; they are the building blocks of formulas.
2. A literal is a formula that is either atomic or of the form where is atomic. If a literal is atomic, it is called a positive literal. Otherwise, it is a negative literal.
3. A finite disjunction of literals is called a clause. In other words, a clause is a formula of the form , where each is a literal.
4. A qunatifier-free formula is a formula that does not contain the symbols or .
5. If we identify a formula with its double negation , then it can be shown that any quantifier-free formula can be identified with a formula that is in conjunctive normal form, that is, a finite conjunction of clauses. For a proof, see this link