1. A brief introduction to clausal logic

In this chapter, we will introduce clausal logic as a formalism for representing and reasoning with knowledge. The aim of this chapter is to acquaint the reader with the most important concepts, without going into too much detail. The theoretical aspects of clausal logic, and the practical aspects of Logic Programming, will be discussed in Chapters 2 and 3.

Figure 1.1 Part of the London Underground. Reproduced by permission of London Regional Transport (LRT Registered User No. 94/1954).

Our Universe of Discourse in this chapter will be the London Underground, of which a small part is shown in Figure 1.1. Note that this picture contains a wealth of information, about lines, stations, transit between lines, relative distance, etc. We will try to capture this information in logical statements. Basically, Figure 1.1 specifies which stations are directly connected by which lines. If we follow the lines from left to right (Northern downwards), we come up with the following 11 formulas:

connected(bond_street,oxford_circus,central).
connected(oxford_circus,tottenham_court_road,central).
connected(bond_street,green_park,jubilee).
connected(green_park,charing_cross,jubilee).
connected(green_park,piccadilly_circus,piccadilly).
connected(piccadilly_circus,leicester_square,piccadilly).
connected(green_park,oxford_circus,victoria).
connected(oxford_circus,piccadilly_circus,bakerloo).
connected(piccadilly_circus,charing_cross,bakerloo).
connected(tottenham_court_road,leicester_square,northern).
connected(leicester_square,charing_cross,northern).


/** <examples>
?-connected(bond_street,Y,L).
?-connected(X,piccadilly_circus,L).
?-connected(X,Y,piccadilly).
?-connected(X,Y,L),connected(Y,Z,L).
*/

Let’s define two stations to be nearby if they are on the same line, with at most one station in between. This relation can also be represented by a set of logical formulas:

nearby(bond_street,oxford_circus).
nearby(oxford_circus,tottenham_court_road).
nearby(bond_street,tottenham_court_road).
nearby(bond_street,green_park).
nearby(green_park,charing_cross).
nearby(bond_street,charing_cross).
nearby(green_park,piccadilly_circus).
nearby(piccadilly_circus,leicester_square).
nearby(green_park,leicester_square).
nearby(green_park,oxford_circus).
nearby(oxford_circus,piccadilly_circus).
nearby(piccadilly_circus,charing_cross).
nearby(oxford_circus,charing_cross).
nearby(tottenham_court_road,leicester_square).
nearby(leicester_square,charing_cross).
nearby(tottenham_court_road,charing_cross).


/** <examples>
?-nearby(bond_street,Y).
?-nearby(X,piccadilly_circus).
?-nearby(X,Y).
?-nearby(X,Y),nearby(Y,Z).
*/

These 16 formulas have been derived from the previous 11 formulas in a systematic way. If X and Y are directly connected via some line L, then X and Y are nearby. Alternatively, if there is some Z in between, such that X and Z are directly connected via L, and Z and Y are also directly connected via L, then X and Y are also nearby. We can formulate this in logic as follows:

nearby(X,Y):-connected(X,Y,_L).
nearby(X,Y):-connected(X,Z,L),connected(Z,Y,L).


/** <examples>
?-nearby(tottenham_court_road,leicester_square).
?-nearby(tottenham_court_road,W).
?-nearby(X,leicester_square).
*/

In these formulas, the symbol ‘:-’ should be read as ‘if’, and the comma between connected(X,Z,L) and connected(Z,Y,L) should be read as ‘and’. The uppercase letters stand for universally quantified variables, such that, for instance, the second formula means:

For any values of X, Y, Z and L, X is nearby Y if X is directly connected to Z via L, and Z is directly connected to Y via L.

We now have two definitions of the nearby-relation, one which simply lists all pairs of stations that are nearby each other, and one in terms of direct connections. Logical formulas of the first type, such as

nearby(bond_street,oxford_circus).

will be called facts, and formulas of the second type, such as

nearby(X,Y):-connected(X,Z,L),connected(Z,Y,L).

will be called rules. Facts express unconditional truths, while rules denote conditional truths, i.e. conclusions which can only be drawn when the premises are known to be true. Obviously, we want these two definitions to be equivalent: for each possible query, both definitions should give exactly the same answer. We will make this more precise in the next section.

Exercise 1.1

Two stations are ‘not too far’ if they are on the same or a different line, with at most one station in between. Define rules for the predicate not_too_far.

not_too_far(X,Y):-true.  % replace 'true' with your definition
not_too_far(X,Y):-true.  % add more clauses as needed


/** <examples>
?-not_too_far(X,Y).
*/

Tip

Notice that if X and Y are connected via line L, then the reverse should also hold: Y and X are connected via the same line L. This can be expressed logically as follows:

connected(Y,X,L):-connected(X,Y,L).


/** <examples>
?-connected(X,Y,central).                 % gives infinitely many answers
?-connected(bond_street,charing_cross,L). % should fail, but doesn't terminate
*/

While this makes logical sense, it causes problems computationally:

• there are now infinitely many ways to demonstrate that two stations are connected, as you can always use the rule twice more;

• for any pair of stations that are not connected, the rule suggests to swap them again and again to see if that leads to a connection, so this never terminates.

The two queries in the SWISH box illustrate these two issues, so be sure to try them out.

Procedural issues such as these will be discussed in more detail in Chapter 3. For now we will stick to the above 11 facts, which means that we only consider trains that (roughly) move from west to east and from south to north.