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 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 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.
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,
mother(anne, bridget).
mother(abigail, bridget).
mother(bridget, carol).
grandmother(C, GM) <= mother(C, M) and mother(M, GM).
? grandmother(anne, carol).
{ Grand Mother }
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.
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.
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:
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.
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).
{ The Aunt/Uncle Relation. }
When the program is run it produces the following answers.
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:
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"!
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.
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:
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).
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.
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].
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:
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.