Examples of Horn Clauses

A logic programming language is a notational system for writing logical statements together with specified algorithms for implementing inference rules.
Horn clauses can be used to express logical statements formally and concisely. So the following procedures are taken for writing a logic program: 
Logical Statements
⇓
First-order Predicate Calculus
⇓
Horn Clauses
⇓
A Logic Program

Example I
Consider the logical description for the Euclidean algorithm to compute the greatest common divisor of two positive integers u and v: 
  The gcd of u and 0 is u.
  The gcd of u and v, if v is not 0, is the same as
     the gcd of v and the remainder of dividing v into u.
Translating this into first-order predicate calculus gives 
  for all u, gcd( u, 0, u ).
  for all u, for all v, for all w,
    not zero( v ) and gcd( v, u mod v, w ) → gcd( u, v, w ).
gcd(u,v,w) is a predicate expressing that w is the gcd of u and v. Translate these statements into Horn clauses by dropping the quantifiers: 
  gcd( u, 0, u ).
  not zero( v ) and gcd( v, u mod v, w ) → gcd( u, v, w ).