First-Order Logic Definitions

Every expression is composed of constants, variables, predicates, and functions.
A term is any constant, or variable, or any function applied to any term.
A literal is any predicate (or its negation) applied to any set of terms.
Female(Mary), ¬Female(x)
A ground literal is a literal that does not contain any variables.
A clause is any disjunction of literals whose variables are universally quantified.
∀ x : Female(x) ∨ Male(x)
A Horn clause is an expression of the form
H ← L1 ∧ L2 ∧ ... ∧ Ln
For any A and B
A ← B ⇒ A ∨ ¬ B
so the horn clause above can be re-written as
H ∧ ¬L1 ∨ ¬L2 ∨ ... ∨ ¬Ln
A substitution is any function that replaces variables by terms e.g., {x/3, y/z} replaces x for 3 and y for z.
A unifying substitution θ for two literals L1 and L2 is one where
L1θ = L2θ