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.