A

Horn clause is a unique kind of

proposition which has either one single proposition on the

left hand side or an empty proposition. When a Horn

clause does contain a proposition on the left side, it is sometimes refered to as a

headed Horn clause. The Horn clause is named after

Alfred Horn who studied this type of

propositional clause (Horn, 1951).

Let "

**:-**" mean "implies" and the comma "

**,**" mean "and". This is the

syntax that the

Prolog programming language uses for its propositions. In mathematical logic "and" implies that both elements must be true in order for the

statement to be true. This is the

logic used in Horn clauses. Below is an example:

hates(John, apples)

**:-** hates(John, fruit)

**,** fruit(apple).

This is read as follows: "John hates fruit, and an apple is a fruit, which implies that John hates apples". Below is an example of a

headless Horn clause:

astronaut(Rick).

This is read as "Rick is an astronaut" and is taken as a statement of

fact.

It is interesting to note that the majority of propositions can be written as Horn clauses. Another point of interest is that the Prolog programming language was designed to use propositions in Horn

clause form, along with an inference rule called

resolution which is used to

prove propositions of this form, as the basis for its

declarative semantics.