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:


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.

Log in or register to write something here or to contact authors.