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.
<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.
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.
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,
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.
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.
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.
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.
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.
The output includes the correct answer.
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
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].
A surprising feature of append is that it can be run "backwards" to take a list apart.
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:
-- LA, 9/2007