(ch: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 {numref}`Chapters %s` and {numref}`%s`.
+++
```{figure} /src/fig/part_i/image002.svg
---
name: 'fig:1.1'
width: 100%
---
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 {numref}`fig: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, {numref}`fig: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:
```{swish} swish:1.0.1
```
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:
```{swish} swish:1.0.2
```
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:
```{swish} swish:1.0.3
---
inherit-id: swish:1.0.1
---
```
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
```Prolog
nearby(bond_street,oxford_circus).
```
will be called *facts*, and formulas of the second type, such as
```Prolog
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} ex:1.1
```
````{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:
```{swish} swish:1.0.added
---
inherit-id: swish:1.0.1
---
```
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 {numref}`Chapter %s`.
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 sourth to north.
````