The utility of the clause-form equivalent representation for logic and theorem proving gave rise to the Prolog language: programming in logic.

Horn Clauses

Prolog is based on a restricted form of clause-form equivalent known as the Horn clause.

• A Horn clause is a disjunction of literals, with at most one positive (non-negated) literal.
• Example: [\(p(X, Y, Z), \neg q(X, Z), \neg r(Z, Y)\)]

Implication Form

In Prolog, Horn clauses are written in implication form:

p(X, Y, Z) :- q(X, Z), r(Z, Y).

The meaning is p(X, Y, Z) is true if q(X, Z) is true and r(Z, Y) is true.

We can see that this is equivalent to a Horn clause by logic rewriting.

• \((q(X, Z) \wedge r(Z, Y)) \implies p(X, Y, Z)\)
• \((\neg (q(X, Z) \wedge r(Z, Y)) \vee p(X, Y)\)
• \(\neg q(X, Z) \vee \neg r(Z, Y) \vee p(X, Y)\)

The final form is a disjunction of literals, with exactly one positive literal.

Prolog Program for Sorting

%  R is the sorted version of Q if 
%     (a) R is a permutation of Q and 
%     (b) R is ordered.
slowsort(Q, R) :- permutation(Q, R), ordered(R).

permutation([], []).

% The list [Y1 | MoreYs] is a permutation of X if:
%     (a) there are lists Xinitial and Xfinal such that
%         the append of Xinitial and [Y1| Xfinal] is X,
%     (b) there is a list XlessY1 that is the append of Xinitial and Xfinal,
%     (c) XlessY1 is a permutation of MoreYs.

permutation(X, [Y1 | MoreYs]) :-
  append(Xinitial, [Y1 | Xfinal], X),
  append(Xinitial, Xfinal, XlessY1),
  permutation(XlessY1, MoreYs).

ordered([]).

ordered([_]).

ordered([A1, A2| MoreAs]) :-
  A1 =< A2, ordered([A2 | MoreAs]).