# Programming in Logic: Prolog

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]).

Updated Thu Nov. 08 2018, 12:02 by cameron.