2.4. Definite clause logic#
In the foregoing three sections, we introduced and discussed three variants of clausal logic, in order of increasing expressiveness. In this section, we will show how an additional restriction on each of these variants will significantly improve the efficiency of a computational reasoning system for clausal logic. This is the restriction to definite clauses, on which Prolog is based. On the other hand, this restriction also means that definite clause logic is less expressive than full clausal logic, the main difference being that clausal logic can handle negative information. If we allow negated literals in the body of a definite clause then we obtain a so-called general clause, which is probably the closest we can get to full clausal logic without having to sacrifice efficiency.
Consider the following program:
married(X);bachelor(X):-man(X),adult(X).
man(peter).
adult(peter).
:-married(maria).
:-bachelor(maria).
man(paul).
:-bachelor(paul).
There are many clauses that are logical consequences of this program. In particular, the following three clauses can be derived by resolution:
married(peter);bachelor(peter).
:-man(maria),adult(maria).
married(paul):-adult(paul).
Exercise 2.12 #
Draw the proof tree for each of these derivations.
In each of these derivations, the first clause in the program is used in a different way. In the first one, only literals in the body are resolved away; one could say that the clause is used from right to left. In the second derivation the clause is used from left to right, and in the third one literals from both the head and the body are resolved away. The way in which a clause is used in a resolution proof cannot be fixed in advance, because it depends on the thing we want to prove (the query in refutation proofs).
On the other hand, this indeterminacy substantially increases the time it takes to find a refutation. Let us decide for the moment to use clauses only in one direction, say from right to left. That is, we can only resolve the negative literals away in a clause, as in the first derivation above, but not the positive literals. But now we have a problem: how are we going to decide whether Peter is married or a bachelor? We are stuck with a clause with two positive literals, representing a disjunctive or indefinite conclusion.
This problem can in turn be solved by requiring that clauses have exactly one positive literal, which leads us into definite clause logic. Consequently, a definite clause
will always be used in the following way: \(A\) is proved by proving each of \(B_1 , \ldots , B_n\). This is called the procedural interpretation of definite clauses, and its simplicity makes the search for a refutation much more efficient than in the indefinite case. Moreover, it allows for an implementation which limits the amount of memory needed, as will be explained in more detail in Chapter 5.
But how do we express in definite clause logic that adult men are bachelors or married? Even if we read the corresponding indefinite clause from right to left only, it basically has two different procedural interpretations:
to prove that someone is married, prove that he is a man and an adult, and prove that he is not a bachelor;
to prove that someone is a bachelor, prove that he is a man and an adult, and prove that he is not married.
We should first choose one of these procedural interpretations, and then convert it into a ‘pseudo-definite’ clause. In case 1, this would be
married(X):-man(X),adult(X),not bachelor(X).
and case 2 becomes
bachelor(X):-man(X),adult(X),not married(X).
These clauses do not conform to the syntax of definite clause logic, because of the negation symbol not. We will call them general clauses.
If we want to extend definite clause logic to cover general clauses, we should extend resolution in order to deal with negated literals in the body of a clause. In addition, we should extend the semantics. This topic will be addressed in Section 8.2. Without going into too much detail here, we will demonstrate that preferring a certain procedural interpretation corresponds to preferring a certain minimal model. Reconsider the original indefinite clause
married(X);bachelor(X):-man(X),adult(X).
Supposing that john is the only individual in the Herbrand universe, and that man(john) and adult(john) are both true, then the models of this clause are
{ man(john), adult(john), married(john) }
{ man(john), adult(john), bachelor(john) }
{ man(john), adult(john), married(john), bachelor(john) }
Note that the first two models are minimal, as is characteristic for indefinite clauses. If we want to make the clause definite, we should single out one of these two minimal models as the intended model. If we choose the first model, in which John is married but not a bachelor, we are actually preferring the general clause
married(X):-man(X),adult(X),not bachelor(X).
Likewise, the second model corresponds to the general clause
bachelor(X):-man(X),adult(X),not married(X).
Write a clause for the statement ‘somebody is innocent unless proven guilty’, and give its intended model (supposing that john is the only individual in the Herbrand universe).
An alternative approach to general clauses is to treat not as a special Prolog predicate, as will be discussed in the next chapter. This has the advantage that we need not extend the proof theory and semantics to incorporate general clauses. However, a disadvantage is that in this way not can only be understood procedurally.