1.1. Answering queries#
A query like ‘which station is nearby Tottenham Court Road?’ will be written as
?-nearby(tottenham_court_road,W).
where the prefix ‘?-’ indicates that this is a query rather than a fact. An answer to this query, e.g. ‘Leicester Square’, will be written { W → leicester_square }, indicating a substitution of values for variables, such that the statement in the query, i.e.
?-nearby(tottenham_court_road,leicester_square).
is true. Now, if the nearby-relation is defined by means of a list of facts, answers to queries are easily found: just look for a fact that matches the query, by which is meant that the fact and the query can be made identical by substituting values for variables in the query. Once we have found such a fact, we also have the substitution which constitutes the answer to the query.
If rules are involved, query-answering can take several of these steps. For answering the query ?-nearby(tottenham_court_road,W), we match it with the conclusion of the rule
nearby(X,Y):-connected(X,Y,L).
yielding the substitution { X → tottenham_court_road, Y → W }. We then try to find an answer for the premises of the rule under this substitution, i.e. we try to answer the query
?-connected(tottenham_court_road,W,L).
That is, we can find a station nearby Tottenham Court Road, if we can find a station directly connected to it. This second query is answered by looking at the facts for direct connections, giving the answer { W → leicester_square, L → northern }. Finally, since the variable L does not occur in the initial query, we just ignore it in the final answer, which becomes { W → leicester_square } as above. In Figure 1.2, we give a graphical representation of this process. Since we are essentially proving that a statement follows logically from some other statements, this graphical representation is called a proof tree.
Figure 1.2 A proof tree for the query ?-nearby(tottenham_court_road,W).#
The steps in Figure 1.2 follow a very general reasoning pattern:
to answer a query \(\texttt{?-} Q_1, Q_2, \ldots , Q_n\), find a rule \(A \texttt{:-} B_1, \ldots , B_m\) such that \(A\) matches with \(Q_1\), and answer the query \(\texttt{?-} B_1, \ldots , B_m, Q_2, \ldots , Q_n\).
This reasoning pattern is called resolution, and we will study it extensively in Chapters 2 and 3. Resolution adds a procedural interpretation to logical formulas, besides their declarative interpretation (they can be either true or false). Due to this procedural interpretation, logic can be used as a programming language. In an ideal logic programming system, the procedural interpretation would exactly match the declarative interpretation: everything that is calculated procedurally is declaratively true, and vice versa. In such an ideal system, the programmer would just bother about the declarative interpretation of the formulas she writes down, and leave the procedural interpretation to the computer. Unfortunately, in current logic programming systems the procedural interpretation does not exactly match the declarative interpretation: for example, some things that are declaratively true are not calculated at all, because the system enters an infinite loop. Therefore, the programmer should also be aware of the procedural interpretation given by the computer to her logical formulas.
The resolution proof process makes use of a technique that is known as reduction to the absurd: suppose that the formula to be proved is false, and show that this leads to a contradiction, thereby demonstrating that the formula to be proved is in fact true. Such a proof is also called a proof by refutation. For instance, if we want to know which stations are nearby Tottenham Court Road, we negate this statement, resulting in ‘there are no stations nearby Tottenham Court Road’. In logic, this is achieved by writing the statement as a rule with an empty conclusion, i.e. a rule for which the truth of its premises would lead to falsity:
:-nearby(tottenham_court_road,W).
Thus, the symbols ‘?-’ and ‘:-’ are in fact equivalent. A contradiction is found if resolution leads to the empty rule, of which the premises are always true (since there are none), but the conclusion is always false. Conventionally, the empty rule is written as ‘\(\square\)’.
At the beginning of this section, we posed the question: can we show that our two definitions of the nearby-relation are equivalent? As indicated before, the idea is that to be equivalent means to provide exactly the same answers to the same queries. To formalise this, we need some additional definitions. A ground fact is a fact without variables. Obviously, if G is a ground fact, the query ?-G never returns a substitution as answer: either it succeeds (G does follow from the initial assumptions), or it fails (G does not). The set of ground facts G for which the query ?-G succeeds is called the success set. Thus, the success set for our first definition of the nearby-relation consists simply of those 16 formulas, since they are ground facts already, and nothing else is derivable from them. The success set for the second definition of the nearby-relation is constructed by applying the two rules to the ground facts for connectedness. Thus we can say: two definitions of a relation are (procedurally) equivalent if they have the same success set (restricted to that relation).