Introduction.

Horn clause form is a sublanguage of first-order predicate logic. It is particularly convenient for manipulation by computer and a successful programming language Prolog, from programming in logic, has been based on it. Predicate logic is closely linked to the theory of relations. Prolog is therefore suitable for use with relational databases and has given rise to the field of deductive databases. Prolog is also much used in artificial intelligence applications.

Horn Clause Form.

<Exp>     ::= <rule> |
              <query>
<rule>    ::= <atom> |             eg.parents(fred,anne,bill)
              <atom> <= <literals> eg.     odd(s(N))<=even(N)
<query>   ::= ? <literals>         eg.        ?odd(s(s(s(0)))
<literal> ::= atom | not <atom>
<literals>::= <literal> [and <literals>]
<atom>    ::= <predicate_ident> [ (<terms>) ]  eg.diff(X,X,1)
<term>    ::= <ident> (<terms>)  | <constant> | <variable>
<terms>   ::= <term> [, <terms>]

— Horn Clause Form. —

Horn clause form permits the statement of simple atomic facts and of simple implications. These restricted forms are in fact sufficient to express any first-order predicate logic expression although several Horn clause expressions may be needed to do so.

All variables are implicitly quantified and quantifiers are omitted.

quantification rule, query <= removed, ¬ query, contradicted implicit: p(X) <= q(X,Y) p(X) or not q(X,Y) ? p(X) ? not p(X) explicit: ∀ X p(X) <= ∃ Y q(X,Y) ∀ X ∀ Y p(X) or not q(X,Y) ? ∃ X p(X) ? ∀ X not p(X)

— Quantification. —

A variable which appears to the left of '<=' is universally quantified. A variable which appears in a query or only to the right of '<=' is existentially quantified. The proof of a query is equivalent to a proof by contradiction that the negated query fails.

	∀ C ∀ GP grandparent(C,GP) <= ∃ P parent(C,P) and parent(P,GP)
=	∀ C ∀ GP grandparent(C,GP) or not(∃ P parent(C,P) and parent(P,GP))
=	∀ C ∀ GP ∀ P grandparent(C,GP) or not parent(C,P) or not parent(P,GP)

 

— Example with Explicit Quantification. —

Note that every variable in a transformed fact, rule or query is universally (∀) quantified, so quantifiers may as well be omitted.

A Prolog Subset.

A grammar for a small Prolog language is given below; it follows the grammar for Horn clause form closely. Variable names begin with a capital letter. It simplifies matters to make a program consist of zero or more rules followed by a single query; in other systems queries can be interspersed with the rules. Note also that most Prologs use ':-' instead of '<=' and use ',' instead of 'and' to separate atoms.

<Program> ::= [ <rules> ] <query>

<rule>    ::= <atom> . | <atom> <= <literals> .
<rules>   ::= <rule> [ <rules> ]
<query>   ::= ? <literals> .
<literal> ::= <atom> | not <atom>
<literals>::= <literal> [ and <literals> ]
<atom>    ::= <ident> | <ident> ( <terms> )
<term>    ::= <ident> | <numeral> |      --constants
              <ident> ( <terms> ) |      --functions
              <IDENT>                    --variables
<terms>   ::= <term> [, <terms> ]

— Prolog-S Syntax. —

Declarative and Procedural Semantics.

The term declarative semantics refers to interpreting Prolog statements as formal Mathematical predicate logic. Other statements that logically follow from the program are considered to be true. Consider for example,

program: [GM.pro]

mother(anne, bridget). mother(abigail, bridget). mother(bridget, carol). grandmother(C, GM) <= mother(C, M) and mother(M, GM). ? grandmother(anne, carol). {<B> Grand Mother </B>}

output area

The query logically follows from the other statements because it matches the general rule if C is anne, GM is carol, and M is bridget.

[Exercise: Now change the query above to ask "of whom is carol a grandmother?"]

The term procedural semantics refers to interpreting Prolog statements as procedure (subroutine, method) definitions to be called and run. The three Prolog statements above can be thought of as definitions of procedures 'mother' and 'grandmother'. In order to answer the previous query, call the procedure 'grandmother' which calls 'mother' twice. Procedural semantics require notions of the order of execution, a search strategy and so on.

Declarative semantics are easier to think about and to program in terms of and procedural semantics are needed for implementations. Unfortunately there is a gap between the two semantics. In some problems it is necessary to consider the procedural semantics to be able to write a correct Prolog program. Much research is aimed at reducing this gap.

Prolog Programming Techniques.

Family relationships can be used to illustrate Prolog's ability to define basic relations such as parenthood and derived relations such as grand-parent-hood. A child has two parents - a mother and a father. A parent is either a mother or a father. A grand-parent of a child is a parent of a parent of the child. These rules can easily be expressed in Prolog.

program: [GP.pro]

parents(william, diana, charles). parents(henry, diana, charles). parents(charles, elizabeth, philip). parents(diana, frances, edward). parent(C,M) <= parents(C,M,D). parent(C,D) <= parents(C,M,D). grandparent(C,GP) <= parent(C,P) and parent(P,GP). ?grandparent(william, Who). {<B> Grand-Parent Relation. </B>}

output area

Note that a parent is either a mother or a father. This is expressed by two rules in Prolog. A mother is a parent and it is also true that a father is a parent.

The query '? grandparent(william, Who)' asks if william has a grand-parent and if so who? William has four grand-parents and the simple Prolog interpreter described later finds them all:

grandparen(william, frances) yes
grandparen(william, edward) yes
grandparen(william, elizabeth) yes
grandparen(william, philip) yes

— Solutions to ? grandparent(william, Who). —

Duplicate Solutions.

The definition of aunts and uncles is slightly more difficult than grand-parents. A sibling of a parent is an aunt or an uncle. Two sibling have the same parents. The spouse of an aunt or uncle is also an aunt or uncle. If naively coded in Prolog, this rule allows infinite loops - an aunt is married to an uncle is married to an aunt is married to ... . A solution is to distinguish between the direct relation and the relation by marriage.

program: [Aunt.pro]

parents(william, diana, charles). parents(henry, diana, charles). parents(charles, elizabeth, philip). parents(diana, frances, edward). parents(anne, elizabeth, philip). parents(andrew, elizabeth, philip). parents(edwardW, elizabeth, philip). married(diana, charles). married(elizabeth, philip). married(frances, edward). married(anne, mark). parent(C,M) <= parents(C,M,D). parent(C,D) <= parents(C,M,D). sibling(X,Y) <= parents(X,M,D) and parents(Y,M,D). {NB. sibling(X, X)} aORuDirect(C, A) <= parent(C,P) and sibling(P,A). aORuMarr(C, A) <= aORuDirect(C,X) and married(X,A). aORuMarr(C, A) <= aORuDirect(C,X) and married(A,X). aORu(C,A) <= aORuDirect(C,A). aORu(C,A) <= aORuMarr(C,A). ? aORu(william, A). {<B> The Aunt/Uncle Relation. </B>}

output area

When the program is run it produces the following answers.

aORu(william, diana) yes
aORu(william, charles) yes
aORu(william, anne) yes
aORu(william, andrew) yes
aORu(william, edwardW) yes
aORu(william, charles) yes
aORu(william, mark) yes
aORu(william, diana) yes

— William's supposed Aunts and Uncles. —

Note that this includes the correct aunts and uncles - Andrew, Anne, Edward (Windsor) and Mark - but also includes Charles and Diana, twice. The reason is that an individual is considered to be his or her own sibling (same parents) which is not what we would expect. This makes Diana a direct aunt and Charles a direct uncle. Diana is married to Charles and therefore is also an aunt by marriage and Charles is similarly an uncle by marriage. The way to cure this problem is to state some negative information: Siblings cannot be the same, they must differ.

equal(X, X).

sibling(X, Y) <= parents(X, M, D) and parents(Y, M, D) and not equal(X, Y).

 

— Use of Negative Information. —

 

query: ? sibling(X, Y).

 

part output:

sibling(william, henry) yes

sibling(henry, william) yes

sibling(charles, anne) yes

sibling(charles, andrew) yes

...

 

— Siblings. —

Using this technique with the family we get:

program: [Aunt2.pro}

parents(william, diana, charles). parents(henry, diana, charles). parents(charles, elizabeth, philip). parents(diana, frances, edward). parents(anne, elizabeth, philip). parents(andrew, elizabeth, philip). parents(edwardW, elizabeth, philip). married(diana, charles). married(elizabeth, philip). married(frances, edward). married(anne, mark). parent(C,M) <= parents(C,M,D). parent(C,D) <= parents(C,M,D). equal(X, X). sibling(X,Y) <= parents(X,M,D) and parents(Y,M,D) and not equal(X,Y). aORuDirect(C, A) <= parent(C,P) and sibling(P,A). aORuMarr(C, A) <= aORuDirect(C,X) and married(X,A). aORuMarr(C, A) <= aORuDirect(C,X) and married(A,X). aORu(C,A) <= aORuDirect(C,A). aORu(C,A) <= aORuMarr(C,A). ? aORu(william, A). {<B> The Aunt/Uncle Relation. </B>}

output area

aORu(william, anne) yes

aORu(william, andrew) yes

aORu(william, edwardW) yes

aORu(william, mark) yes

 

— William's genuine Aunts and Uncles. —

Negation (not, ¬) can be implemented using the negation by failure rule which attempts to prove 'not equal(charles, charles', say, by first proving 'equal(charles, charles)'. The latter succeeds and so 'not equal(charles, charles)' fails and is considered false. In general, 'not p(...)' succeeds, and is considered true, if and only if 'p(...)' fails. For example, 'equal(charles, edwardW)' fails and so 'not equal(charles, edwardW)' succeeds.

Negation by failure is not guaranteed to behave correctly if there is an unbound variable in the negated atom. In particular, if the negated atom appeared immediately after the '<=' in the improved rule for sibling then the rule would not work correctly.

sibling (X, Y) <= not equal(X, Y) and parents(X, M, D) and parents(Y, M, D).

 

— Rule unsuitable for (simple) negation by failure. —

With this rule and assuming that X and Y are unbound, it is possible to satisfy 'equal(X,Y)' by binding X to Y and therfore the 'not equal(X,Y)' and the rule fail in Prolog. From the logic point of view, there are many ways for 'not equal(X,Y)' to succeed, for example with X bound to 'william' and Y bound to 'plus(fred,7)'. Only when X and Y are bound to constant or ground terms is negation by failure guaranteed to work correctly. Note that some Prolog interpreters delay any negated atom that contains an unbound variable, in the hope that the variable will become bound, in an attempt to reduce this problem.

More formally,

not ∃ X such that p(X)

is equivalent to

∀ X not p(X)

(but is not equivalent to ∃ X such that not p(X)),

and

not ∀ X p(X)

is equivalent to

∃ X such that not p(X)

(but is not equivalent to ∀ X not p(X)).

Unground variables spoil the otherwise simple negation by failure rule, and this unfortunate interaction can be considered to be a bug, or something to try to avoid, or a "feature"!

Catch-Alls.

A symbolic differentiator can easily be written in Prolog. Most systems allow the use of infix operators but prefix operators plus, times and so on are sufficient and are used here.

program: [Diff.pro]

diff(plus(A,B), X, plus(DA, DB)) <= diff(A, X, DA) and diff(B, X, DB). diff(times(A,B), X, plus(times(A, DB), times(DA, B))) <= diff(A, X, DA) and diff(B, X, DB). equal(X, X). diff(X, X, 1). diff(Y, X, 0) <= not equal(Y, X). ? diff( plus(times(x, x), times(3,x)), x, Dx). {<B> Symbolic Differentiator. </B>}

output area

The output includes the correct answer.

diff(plus(times(x, x), times(3, x)), x, plus(plus(times(x, 1), times(1, x)), plus(times(3, 1), times(0, x)))) yes

 

equivalent infix: diff(x*x+3*x, x, x*1+1*x+3*1+0*3)

 

— d/dx of x*x+3*x —

This is correct although it could usefully be simplified to 2*x+3; it is straightforward to write a simplifier for polynomials in Prolog if the ability to do arithmetic is provided. The output also includes some incorrect answers not shown. The reason is that the rule diff(Y,X,0) catches too many cases. It should be more correctly stated as

diff(Y, X, 0) <= atomic(Y) and not equal(Y,X).

 

— Correct dy/dx Rule. —

This requires negation and also the predicate atomic:

 

atomic(x). atomic(y). atomic(3).

 

— Some Atomic Terms. —

Now we have:

program: [Diff2.pro]

diff(plus(A,B), X, plus(DA, DB)) <= diff(A, X, DA) and diff(B, X, DB). diff(times(A,B), X, plus(times(A, DB), times(DA, B))) <= diff(A, X, DA) and diff(B, X, DB). atomic(x). atomic(y). atomic(3). equal(X, X). diff(X, X, 1). diff(Y, X, 0) <= atomic(Y) and not equal(Y, X). ? diff( plus(times(x, x), times(3,x)), x, Dx). {<B> Symbolic Differentiator. </B>}

output area

Atomic cannot in general be defined by the user but is often part of a Prolog system. Integers and other constants are atomic. Note the slight conflict of terminology between an atom (a predicate, possibly negated), and an atomic term (value).

Running Forwards and Backwards.

It is possible to do list processing in Prolog. The append predicate joins two lists together. The function c can stand for the list constructor, often called cons. The result of appending nil and a list B is just B. The result of appending c(H,T) and B is c(H,TB) where TB is the result of appending T and B.

  c(H, T) + B
       ------
= c(H,  T+B  )

— Appending to a non-null List. —

program: [AppendF.pro]

append(c(H,T), B, c(H,TB)) <= append(T, B, TB). append(nil, B, B). ? append( c(1, c(2, nil)), c(3, c(4, nil)), X). {<B> Append run Forwards. </B>}

output area

The result of appending the lists c(1,c(2,nil)) and c(3,c(4,nil)) is c(1,c(2,c(3,c(4,nil)))). Note that some Prolog systems provide a nicer syntax for lists, e.g., [1,2,3,4].

append(c(1, c(2, nil)), c(3, c(4, nil)), c(1, c(2, c(3, c(4, nil))))) yes

 

— Append two Lists. —

A surprising feature of append is that it can be run "backwards" to take a list apart.

program: [AppendB.pro]

append(c(H,T), B, c(H,TB)) <= append(T, B, TB). append(nil, B, B). ? append( X, Y, c(1, c(2, c(3, nil))) ). {<B> Append run Backwards. </B>}

output area

What two lists, X and Y, when appended result in the list c(1,c(2,c(3,nil))))? There are four ways in which the list c(1,c(2,c(3,nil)))) can be made up of two other lists:

1. append(c(1, c(2, c(3, nil))), nil, c(1, c(2, c(3, nil)))) yes
2. append(c(1, c(2, nil)), c(3, nil), c(1, c(2, c(3, nil)))) yes
3. append(c(1, nil), c(2, c(3, nil)), c(1, c(2, c(3, nil)))) yes
4. append(nil, c(1, c(2, c(3, nil))), c(1, c(2, c(3, nil)))) yes

— Dismantle a List. —

Exercises

1. Define the relation niece-or-nephew in Prolog.

2. Define the relation cousin in Prolog.

3. Major Projects:
   Modify the interpreter to delay any negated atom until its variables are all bound (if ever).

   Add predicates 'int' and 'is' to Prolog-S. 'int(N)' succeeds if and only if N is bound to an integer. 'is(X,E)' or 'X is E' succeeds if and only if E is an arithmetic expression containing only operators, numbers and variables bound to numbers and in that case X is unified with the expression's value.

   Use 'int' and 'is' to write a simplifier in Prolog to go with the symbolic differentiator.