My normal tendency is to write long posts that I never finish. I’ll start off this series with small posts to see if I can break the habit.

The idea of Horn clauses emerged from model theory, so I will begin there. Model theory considers ideas that can expressed in very limited languages. You begin with a small vocabulary of constants, function symbols and relation symbols, known as the *signature*. For example, you can express the theory of groups in terms of two function symbols and one constant: the group product, the inverse function, and a constant that represents the unit. The theory of directed graphs can be described by a single relation symbol *R(x,y)* that expresses whether a directed edge begins at *x* and ends at *y*.

When coupled with first-order logic, even a very limited language can be very expressive. Set theory itself, for example, can be expressed using a single relation symbol (set membership). Horn clauses are special first-order logical statements that are not nearly as expressive, but still cover very many cases, as we shall see.