(sec: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: ```Prolog 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: ```Prolog married(peter);bachelor(peter). :-man(maria),adult(maria). married(paul):-adult(paul). ``` ```{exercise} ex:2.12 ``` +++ 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 $$ A \texttt{:-} B_1 , \ldots , B_n $$ 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 {numref}`Chapter %s`. +++ 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: 1. to prove that someone is married, prove that he is a man and an adult, and prove that he is not a bachelor; 1. 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 ```Prolog married(X):-man(X),adult(X),not bachelor(X). ``` and case 2 becomes ```Prolog 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 clause*s. +++ 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 {numref}`sec: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 ```Prolog 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 ```Prolog { 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 ```Prolog married(X):-man(X),adult(X),not bachelor(X). ``` Likewise, the second model corresponds to the general clause ```Prolog bachelor(X):-man(X),adult(X),not married(X). ``` ```{exercise} ex:2.13 ``` +++ 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.