Propositional clausal logic
Contents
2.1. Propositional clausal logic#
Informally, a proposition is any statement which is either true or false, such as ‘\(2 + 2 = 4\)’ or ‘the moon is made of green cheese’. These are the building blocks of propositional logic, the weakest form of logic.
Syntax#
Propositions are abstractly denoted by atoms, which are single words starting with a lowercase character. For instance, married is an atom denoting the proposition ‘he/she is married’; similarly, man denotes the proposition ‘he is a man’. Using the special symbols ‘:-’ (if), ‘;’ (or) and ‘,’ (and), we can combine atoms to form clauses. For instance,
married;bachelor:-man,adult.
is a clause, with intended meaning: ‘somebody is married or a bachelor if he is a man and an adult’1. The part to the left of the if-symbol ‘:-’ is called the head of the clause, and the right part is called the body of the clause. The head of a clause is always a disjunction (or) of atoms, and the body of a clause is always a conjunction (and).
Tip
This example, which is used throughout Chapters 2 and 3, assumes that bachelors are unmarried men. While this is still logically correct, it is perhaps time to look for a slightly less dated running example…
Translate the following statements into clauses, using the atoms person, sad and happy:
persons are happy or sad;
no person is both happy and sad;
sad persons are not happy;
non-happy persons are sad.
A program is a set of clauses, each of them terminated by a period. The clauses are to be read conjunctively; for example, the program
woman;man:-human.
human:-woman.
human:-man.
has the intended meaning ‘(if someone is human then she/he is a woman or a man) and (if someone is a woman then she is human) and (if someone is a man then he is human)’, or, in other words, ‘someone is human if and only if she/he is a woman or a man’.
Semantics#
The Herbrand base of a program \(P\) is the set of atoms occurring in \(P\). For the above program, the Herbrand base is { woman, man, human }. A Herbrand interpretation (or interpretation for short) for \(P\) is a mapping from the Herbrand base of \(P\) into the set of truth values { true, false }. For example, the mapping
{ woman → true, man → false, human → true }
is a Herbrand interpretation for the above program.
A Herbrand interpretation can be viewed as describing a possible state of affairs in the Universe of Discourse (in this case: ‘she is a woman, she is not a man, she is human’). Since there are only two possible truth values in the semantics we are considering, we could abbreviate such mappings by listing only the atoms that are assigned the truth value true; by definition, the remaining ones are assigned the truth value false. Under this convention, which we will adopt in this book, a Herbrand interpretation is simply a subset of the Herbrand base. Thus, the previous Herbrand interpretation would be represented as { woman, human }.
Since a Herbrand interpretation assigns truth values to every atom in a clause, it also assigns a truth value to the clause as a whole. The rules for determining the truth value of a clause from the truth values of its atoms are not so complicated, if you keep in mind that the body of a clause is a conjunction of atoms, and the head is a disjunction. Consequently, the body of a clause is true if every atom in it is true, and the head of a clause is true if at least one atom in it is true. In turn, the truth value of the clause is determined by the truth values of head and body. There are four possibilities:
the body is true, and the head is true;
the body is true, and the head is false;
the body is false, and the head is true;
the body is false, and the head is false.
The intended meaning of the clause is ‘if body then head’, which is obviously true in the first case, and false in the second case.
What about the remaining two cases? They cover statements like ‘if the moon is made of green cheese then \(2 + 2 = 4\)’, in which there is no connection at all between body and head. One would like to say that such statements are neither true nor false. However, our semantics is not sophisticated enough to deal with this: it simply insists that clauses should be assigned a truth value in every possible interpretation. Therefore, we consider the clause to be true whenever its body is false. It is not difficult to see that under these truth conditions a clause is equivalent with the statement ‘head or not body’. For example, the clause married;bachelor:-man,adult can also be read as ‘someone is married or a bachelor or not a man or not an adult’. Thus, a clause is a disjunction of atoms, which are negated if they occur in the body of the clause. Therefore, the atoms in the body of the clause are often called negative literals, while those in the head of the clause are called positive literals.
To summarise: a clause is assigned the truth value true in an interpretation, if and only if at least one of the following conditions is true: (a) at least one atom in the body of the clause is false in the interpretation (cases 3 and 4), or (b) at least one atom in the head of the clause is true in the interpretation (cases 1 and 3). If a clause is true in an interpretation, we say that the interpretation is a model for the clause. An interpretation is a model for a program if it is a model for each clause in the program. For example, the above program has the following models: \(\emptyset\) (the empty model, assigning false to every atom), { woman, human }, { man, human }, and { woman, man, human }. Since there are eight possible interpretations for a Herbrand base with three atoms, this means that the program contains enough information to rule out half of these.
Adding more clauses to the program means restricting its set of models. For instance, if we add the clause woman (a clause with an empty body) to the program, we rule out the first and third model, which leaves us with the models { woman, human }, and { woman, man, human }. Note that in both of these models, human is true. We say that human is a logical consequence of the set of clauses. In general, a clause \(C\) is a logical consequence of a program \(P\) if every model of the program is also a model of the clause; we write \(P \models C\).
Given the program
married;bachelor:-man,adult.
man.
:-bachelor.
determine which of the following clauses are logical consequences of this program:
married:-adult;married:-bachelor;bachelor:-man;bachelor:-bachelor.
Of the two remaining models, obviously { woman, human } is the intended one; but the program does not yet contain enough information to distinguish it from the non-intended model { woman, man, human }. We can add yet another clause, to make sure that the atom man is mapped to false. For instance, we could add
:-man.
(it is not a man) or
:-man,woman.
(nobody is both a man and a woman). However, explicitly stating everything that is false in the intended model is not always feasible. Consider, for example, an airline database consulted by travel agencies: we simply want to say that if a particular flight (i.e., a combination of plane, origin, destination, date and time) is not listed in the database, then it does not exist, instead of listing all the dates that a particular plane does not fly from Amsterdam to London.
So, instead of adding clauses until a single model remains, we want to add a rule to our semantics which tells us which of the several models is the intended one. The airline example shows us that, in general, we only want to accept something as true if we are really forced to, i.e. if it is true in every possible model. This means that we should take the intersection of every model of a program in order to construct the intended model. In the example, this is { woman, human }. Note that this model is minimal in the sense that no subset of it is also a model. Therefore, this semantics is called a minimal model semantics.
Unfortunately, this approach is only applicable to a restricted class of programs. Consider the following program:
woman;man:-human.
human.
This program has three models: { woman, human }, { man, human }, and { woman, man, human }. The intersection of these models is { human }, but this interpretation is not a model of the first clause! The program has in fact not one, but two minimal models, which is caused by the fact that the first clause has a disjunctive head. Such a clause is called indefinite, because it does not permit definite conclusions to be drawn.
On the other hand, if we would only allow definite clauses, i.e. clauses with a single positive literal, minimal models are guaranteed to be unique. We will deal with definite clauses in Section 2.4, because Prolog is based on definite clause logic. In principle, this means that clauses like woman;man:-human are not expressible in Prolog. However, such a clause can be transformed into a ‘pseudo-definite’ clause by moving one of the literals in the head to the body, extended with an extra negation. This gives the following two possibilities:
woman:-human,not(man).
man:-human,not(woman).
In Prolog, we have to choose between these two clauses, which means that we have only an approximation of the original indefinite clause. Negation in Prolog is an important subject with many aspects. In Chapter 3, we will show how Prolog handles negation in the body of clauses. In Chapter 8, we will discuss particular applications of this kind of negation.
Proof theory#
Recall that a clause \(C\) is a logical consequence of a program \(P\) (\(P \models C\)) if every model of \(P\) is a model of \(C\). Checking this condition is, in general, unfeasible. Therefore, we need a more efficient way of computing logical consequences, by means of inference rules. If \(C\) can be derived from \(P\) by means of a number of applications of such inference rules, we say that \(C\) can be proved from \(P\). Such inference rules are purely syntactic, and do not refer to any underlying semantics.
The proof theory for clausal logic consists of a single inference rule called resolution. Resolution is a very powerful inference rule. Consider the following program:
married;bachelor:-man,adult.
has_wife:-man,married.
This simple program has no less than 26 models, each of which needs to be considered if we want to check whether a clause is a logical consequence of it.
The following clause is a logical consequence of this program:
has_wife;bachelor:-man,adult.
By means of resolution, it can be produced in a single step. This step represents the following line of reasoning: ‘if someone is a man and an adult, then he is a bachelor or married; but if he is married, he has a wife; therefore, if someone is a man and an adult, then he is a bachelor or he has a wife’. In this argument, the two clauses in the program are related to each other by means of the atom married, which occurs in the head of the first clause (a positive literal) and in the body of the second (a negative literal). The derived clause, which is called the resolvent, consists of all the literals of the two input clauses, except married (the literal resolved upon). The negative literal man, which occurs in both input clauses, appears only once in the derived clause. This process is depicted in Figure 2.1.
Figure 2.1 A resolution step.#
Resolution is most easily understood when applied to definite clauses. Consider the following program:
square:-rectangle,equal_sides.
rectangle:-parallelogram,right_angles.
Applying resolution yields the clause
square:-parallelogram,right_angles,equal_sides.
That is, the atom rectangle in the body of the first clause is replaced by the body of the second clause (which has rectangle as its head). This process is also referred to as unfolding the second clause into the first one (Figure 2.2).
Figure 2.2 Resolution with definite clauses.#
A resolvent resulting from one resolution step can be used as input for the next. A proof or derivation of a clause \(C\) from a program \(P\) is a sequence of clauses such that each clause is either in the program, or the resolvent of two previous clauses, and the last clause is \(C\). If there is a proof of \(C\) from \(P\), we write \(P \vdash C\).
Meta-theory#
It is easy to show that propositional resolution is sound: you have to establish that every model for the two input clauses is a model for the resolvent. In our earlier example, every model of married;bachelor:-man,adult and has_wife:-man,married must be a model of has_wife;bachelor:-man,adult. Now, the literal resolved upon (in this case married) is either assigned the truth value true or false. In the first case, every model of has_wife:-man,married is also a model of has_wife:-man; in the second case, every model of married;bachelor:-man,adult is also a model of bachelor:-man,adult. In both cases, these models are models of a subclause of the resolvent, which means that they are also models of the resolvent itself.
In general, proving completeness is more complicated than proving soundness. Still worse, proving completeness of resolution is impossible, because resolution is not complete at all! For instance, consider the clause a:-a. This clause is a so-called tautology: it is true under any interpretation. Therefore, any model of an arbitrary program \(P\) is a model for it, and thus \(P \models\) a:-a for any program \(P\). If resolution were complete, it would be possible to derive the clause a:-a from some program \(P\) in which the literal a doesn’t even occur! It is clear that resolution is unable to do this.
However, this is not necessarily bad, because although tautologies follow from any set of clauses, they are not very interesting. Resolution makes it possible to guide the inference process, by implementing the question ‘is \(C\) a logical consequence of \(P\)?’ rather than ‘what are the logical consequences of \(P\)?’. We will see that, although resolution is unable to generate every logical consequence of a set of clauses, it is complete in the sense that resolution can always determine whether a specific clause is a logical consequence of a set of clauses.
The idea is analogous to a proof technique in mathematics called ‘reduction to the absurd’. Suppose for the moment that \(C\) consists of a single positive literal a; we want to know whether \(P \models\) a, i.e. whether every model of \(P\) is also a model of a. It is easily checked that an interpretation is a model of a if, and only if, it is not a model of :-a. Therefore, every model of \(P\) is a model of a if, and only if, there is no interpretation which is a model of both :-a and \(P\). In other words, a is a logical consequence of \(P\) if, and only if, :-a and \(P\) are mutually inconsistent (don’t have a common model). So, checking whether \(P \models\) a is equivalent to checking whether \(P \cup\) { :-a } is inconsistent.
Resolution provides a way to check this condition. Note that, since an inconsistent set of clauses doesn’t have a model, it trivially satisfies the condition that any model of it is a model of any other clause; therefore, an inconsistent set of clauses has every possible clause as its logical consequence. In particular, the absurd or empty clause, denoted by \(\square\)2, is a logical consequence of an inconsistent set of clauses. Conversely, if \(\square\) is a logical consequence of a set of clauses, we know it must be inconsistent. Now, resolution is complete in the sense that if P set of clauses is inconsistent, it is always possible to derive \(\square\) by resolution. Since resolution is sound, we already know that if we can derive \(\square\) then the input clauses must be inconsistent. So we conclude: a is a logical consequence of \(P\) if, and only if, the empty clause can be deduced by resolution from \(P\) augmented with :-a. This process is called proof by refutation, and resolution is called refutation complete.
This proof method can be generalised to the case where \(B\) is not a single atom. For instance, let us check by resolution that a:-a is a tautology, i.e. a logical consequence of any set of clauses. Logically speaking, this clause is equivalent to ‘a or not a’, the negation of which is ‘not a and a’, which is represented by two separate clauses :-a and a. Since we can derive the empty clause from these two clauses in a single resolution step without using any other clauses, we have in fact proved that a:-a is a logical consequence of an empty set of clauses, hence a tautology.
Prove by refutation that friendly:-has_friends is a logical consequence of the following clauses:
happy:-has_friends.
friendly:-happy.
Finally, we mention that although resolution can always be used to prove inconsistency of a set of clauses it is not always fit to prove the opposite, i.e. consistency of a set of clauses. For instance, a is not a logical consequence of a:-a; yet, if we try to prove the inconsistency of :-a and a:-a (which should fail) we can go on applying resolution forever! The reason, of course, is that there is a loop in the system: applying resolution to :-a and a:-a again yields :-a. In this simple case it is easy to check for loops: just maintain a list of previously derived clauses, and do not proceed with clauses that have been derived previously.
However, as we will see, this is not possible in the general case of full clausal logic, which is semi-decidable with respect to the question ‘is \(B\) a logical consequence of \(A\)’: there is an algorithm which derives, in finite time, a proof if one exists, but there is no algorithm which, for any \(A\) and \(B\), halts and returns ‘no’ if no proof exists. The reason for this is that interpretations for full clausal logic are in general infinite. As a consequence, some Prolog programs may loop forever (just like some Pascal programs). One might suggest that it should be possible to check, just by examining the source code, whether a program is going to loop or not, but, as Alan Turing showed, this is, in general, impossible (the Halting Problem). That is, you can write programs for checking termination of programs, but for any such termination checking program you can write a program on which it will not terminate itself!
Tip
prop_atom(married).
prop_atom(bachelor).
prop_atom(man).
prop_atom(adult).
% Propositional atoms are trivially ground
ground_atom(A):-prop_atom(A).