atomic formula
Let $\mathrm{\Sigma}$ be a signature^{} and $T(\mathrm{\Sigma})$ the set of terms over $\mathrm{\Sigma}$. The set $S$ of symbols for $T(\mathrm{\Sigma})$ is the disjoint union^{} of $\mathrm{\Sigma}$ and $V$, a countably infinite^{} set whose elements are called variables. Now, adjoin $S$ the set $\{=,(,)\}$, assumed to be disjoint from $S$. An atomic formula $\phi $ over $\mathrm{\Sigma}$ is any one of the following:

1.
either $({t}_{1}={t}_{2})$, where ${t}_{1}$ and ${t}_{2}$ are terms in $T(\mathrm{\Sigma})$,

2.
or $(R({t}_{1},\mathrm{\dots},{t}_{n}))$, where $R\in \mathrm{\Sigma}$ is an $n$ary relation symbol, and ${t}_{i}\in T(\mathrm{\Sigma})$.
Remarks.

1.
Using atomic formulas, one can inductively build formulas^{} using the logical connectives $\vee $, $\mathrm{\neg}$, $\exists $, 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 $\mathrm{\neg}\phi $ where $\phi $ 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 ${\phi}_{1}\vee {\phi}_{2}\vee \mathrm{\cdots}\vee {\phi}_{n}$, where each ${\phi}_{i}$ is a literal.

4.
A qunatifierfree formula is a formula that does not contain the symbols $\exists $ or $\forall $.

5.
If we identify a formula $\phi $ with its double negation $\mathrm{\neg}(\mathrm{\neg}\phi )$, then it can be shown that any quantifierfree 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 (http://planetmath.org/EveryPropositionIsEquivalentToAPropositionInDNF)
Title  atomic formula 
Canonical name  AtomicFormula 
Date of creation  20130322 12:42:54 
Last modified on  20130322 12:42:54 
Owner  CWoo (3771) 
Last modified by  CWoo (3771) 
Numerical id  10 
Author  CWoo (3771) 
Entry type  Definition 
Classification  msc 03C99 
Classification  msc 03B10 
Synonym  quantifier free formula 
Related topic  TermsAndFormulas 
Related topic  CNF 
Related topic  DNF 
Defines  literal 
Defines  clause 
Defines  quantifierfree formula 
Defines  positive literal 
Defines  negative literal 