Prolog
Introduction.
Horn clause form is a sublanguage of firstorder 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 firstorder 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, contradictedimplicit: 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> ]
 — PrologS 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]
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 grandparenthood. A child has two parents  a mother and a father. A parent is either a mother or a father. A grandparent of a child is a parent of a parent of the child. These rules can easily be expressed in Prolog.
program: [GP.pro]
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 grandparent and if so who? William has four grandparents 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 grandparents. 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]
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}
 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"!
CatchAlls.
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]
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]
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 nonnull List. —
program: [AppendF.pro]
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]
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:
 append(c(1, c(2, c(3, nil))), nil, c(1, c(2, c(3, nil)))) yes
 append(c(1, c(2, nil)), c(3, nil), c(1, c(2, c(3, nil)))) yes
 append(c(1, nil), c(2, c(3, nil)), c(1, c(2, c(3, nil)))) yes
 append(nil, c(1, c(2, c(3, nil))), c(1, c(2, c(3, nil)))) yes
 — Dismantle a List. —
Exercises
 Define the relation nieceornephew in Prolog.
 Define the relation cousin in Prolog.
 Major Projects:
Modify the interpreter to delay any negated atom until its variables are all bound (if ever).Add predicates 'int' and 'is' to PrologS. '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.