  where the head A is an atomic formula (atom). In the simplest case, the body Δ is a list of atoms B1,…,Bm, in which case a definition looks like a definite logic program. We often consider an extended case where Δ may also contain some structural implication ‘⇒’, and sometimes even some structural universal implication, which essentially is handled by restricting substitution. If the definition of A has the form