2.2. Relational clausal logic#
Propositional clausal logic is rather coarse-grained, because it takes propositions (i.e. anything that can be assigned a truth value) as its basic building blocks. For example, it is not possible to formulate the following argument in propositional logic:
Peter likes all his students
Maria is one of Peter’s students
Therefore, Peter likes Maria
In order to formalise this type of reasoning, we need to talk about individuals like Peter and Maria, sets of individuals like Peter’s students, and relations between individuals, such as ‘likes’. This refinement of propositional clausal logic leads us into relational clausal logic.
Syntax#
Individual names are called constants; we follow the Prolog convention of writing them as single words starting with a lowercase character (or as arbitrary strings enclosed in single quotes, like 'this is a constant'). Arbitrary individuals are denoted by variables, which are single words starting with an uppercase character. Jointly, constants and variables are denoted as terms. A ground term is a term without variables[1].
Relations between individuals are abstractly denoted by predicates (which follow the same notational conventions as constants). An atom is a predicate followed by a number of terms, enclosed in brackets and separated by commas, e.g. likes(peter,maria). The terms between brackets are called the arguments of the predicate, and the number of arguments is the predicate’s arity. The arity of a predicate is assumed to be fixed, and predicates with the same name but different arity are assumed to be different. A ground atom is an atom without variables.
All the remaining definitions pertaining to the syntax of propositional clausal logic, in particular those of literal, clause and program, stay the same. So, the following clauses are meant to represent the above statements:
likes(peter,S):-student_of(S,peter).
student_of(maria,peter).
The intended meaning of these clauses are, respectively, ‘if S is a student of Peter then Peter likes S’, ‘Maria is a student of Peter’, and ‘Peter likes Maria’. Clearly, we want our logic to be such that the third clause follows logically from the first two, and we want to be able to prove this by resolution. Therefore, we must extend the semantics and proof theory in order to deal with variables.
Logical variables#
Variables in clausal logic are very similar to variables in mathematical formulas: they are placeholders that can be substituted by arbitrary ground terms from the Herbrand universe. It is very important to notice that logical variables are global within a clause (i.e. if the variable occurs at several positions within a clause, it should be substituted everywhere by the same term), but not within a program. This can be clearly seen from the semantics of relational clausal logic, where grounding substitutions are applied to clauses rather than programs. As a consequence, variables in two different clauses are distinct by definition, even if they have the same name. It will sometimes be useful to rename the variables in clauses, such that no two clauses share a variable; this is called standardising the clauses apart.
Semantics#
The Herbrand universe of a program \(P\) is the set of ground terms (i.e. constants) occurring in it. For the above program, the Herbrand universe is { peter, maria }. The Herbrand universe is the set of all individuals we are talking about in our clauses. The Herbrand base of \(P\) is the set of ground atoms that can be constructed using the predicates in \(P\) and the ground terms in the Herbrand universe. This set represents all the things we can say about the individuals in the Herbrand universe.
The Herbrand base of the above program is
{ likes(peter,peter), likes(peter,maria),
likes(maria,peter), likes(maria,maria),
student_of(peter,peter), student_of(peter,maria),
student_of(maria,peter), student_of(maria,maria) }
As before, a Herbrand interpretation is the subset of the Herbrand base whose elements are assigned the truth value true. For instance,
{ likes(peter,maria), student_of(maria,peter) }
is an interpretation of the above program.
Clearly, we want this interpretation to be a model of the program, but now we have to deal with the variables in the program. A substitution is a mapping from variables to terms. For example, { S → maria } and { S → X } are substitutions. A substitution can be applied to a clause, which means that all occurrences of a variable occurring on the left-hand side in a substitution are replaced by the term on the right-hand side. For instance, if \(C\) is the clause
likes(peter,S):-student_of(S,peter).
then the above substitutions yield the clauses
likes(peter,maria):-student_of(maria,peter).
likes(peter,X):-student_of(X,peter).
Notice that the first clause is ground; it is said to be a ground instance of \(C\), and the substitution { S → maria } is called a grounding substitution. All the atoms in a ground clause occur in the Herbrand base, so reasoning with ground clauses is just like reasoning with propositional clauses. An interpretation is a model for a non-ground clause if it is a model for every ground instance of the clause. Thus, in order to show that
M = { likes(peter,maria), student_of(maria,peter) }
is a model of the clause \(C\) above, we have to construct the set of the ground instances of \(C\) over the Herbrand universe { peter, maria }, which is
{ likes(peter,maria):-student_of(maria,peter),
likes(peter,peter):-student_of(peter,peter) }
and show that \(M\) is a model of every element of this set.
Proof theory#
Because reasoning with ground clauses is just like reasoning with propositional clauses, a naive proof method in relational clausal logic would apply grounding substitutions to every clause in the program before applying resolution. Such a method is naive, because a program has many different grounding substitutions, most of which do not lead to a resolution proof. For instance, if the Herbrand universe contains four constants, then a clause with two distinct variables has 16 different grounding substitutions, and a program consisting of three such clauses has 4096 different grounding substitutions.
Instead of applying arbitrary grounding substitutions before trying to apply resolution, we will derive the required substitutions from the clauses themselves. Recall that in order to apply propositional resolution, the literal resolved upon should occur in both input clauses (positive in one clause and negative in the other). In relational clausal logic, atoms can contain variables. Therefore, we do not require that exactly the same atom occurs in both clauses; rather, we require that there is a pair of atoms which can be made equal by substituting terms for variables. For instance, let \(P\) be the following program:
likes(peter,S):-student_of(S,peter).
student_of(maria,T):-follows(maria,C),teaches(T,C).
The second clause is intended to mean: ‘Maria is a student of any teacher who teaches a course she follows’. From these two clauses we should be able to prove that ‘Peter likes Maria if Maria follows a course taught by Peter’. This means that we want to resolve the two clauses on the student_of literals.
The two atoms student_of(S,peter) and student_of(maria,T) can be made equal by replacing S by maria and T by peter, by means of the substitution { S → maria, T → peter }. This process is called unification, and the substitution is called a unifier. Applying this substitution yields the following two clauses:
likes(peter,maria):-student_of(maria,peter).
student_of(maria,peter):-follows(maria,C),teaches(peter,C).
(Note that the second clause is not ground.) We can now construct the resolvent in the usual way, by dropping the literal resolved upon and combining the remaining literals, which yields the required clause
likes(peter,maria):-follows(maria,C),teaches(peter,C).
Write a clause expressing that Peter teaches all the first-year courses, and apply resolution to this clause and the above resolvent.
Consider the following two-clause program \(P'\):
likes(peter,S):-student_of(S,peter).
student_of(X,T):-follows(X,C),teaches(T,C).
which differs from the previous program \(P\) in that the constant maria in the second clause has been replaced by a variable. Since this generalises the applicability of this clause from Maria to any of Peter’s students, it follows that any model for \(P'\) over a Herbrand universe including maria is also a model for \(P\), and therefore \(P' \models P\). In particular, this means that all the logical consequences of \(P'\) are also logical consequences of \(P\). For instance, we can again derive the clause
likes(peter,maria):-follows(maria,C),teaches(peter,C).
from \(P'\) by means of the unifier { S → maria, X → maria, T → peter }.
Unifiers are not necessarily grounding substitutions: the substitution { X → S, T → peter } also unifies the two student_of literals, and the two clauses then resolve to
likes(peter,S):-follows(S,C),teaches(peter,C).
The first unifier replaces more variables by terms than strictly necessary, while the second contains only those substitutions that are needed to unify the two atoms in the input clauses. As a result, the first resolvent is a special case of the second resolvent, that can be obtained by means of the additional substitution { S → maria }. Therefore, the second resolvent is said to be more general than the first[2]. Likewise, the second unifier is called a more general unifier than the first.
As it were, more general resolvents summarise a lot of less general ones. It therefore makes sense to derive only those resolvents that are as general as possible, when applying resolution to clauses with variables. This means that we are only interested in a most general unifier (mgu) of two literals. Such an mgu, if it exists, is always unique, apart from an arbitrary renaming of variables (e.g. we could decide to keep the variable X, and replace S by X). If a unifier does not exist, we say that the two atoms are not unifiable. For instance, the atoms student_of(maria,peter) and student_of(S,maria) are not unifiable.
As we have seen before, the actual proof method in clausal logic is proof by refutation. If we succeed in deriving the empty clause, then we have demonstrated that the set of clauses is inconsistent under the substitutions that are needed for unification of literals. For instance, consider the program
likes(peter,S):-student_of(S,peter).
student_of(S,T):-follows(S,C),teaches(T,C).
teaches(peter,ai_techniques).
follows(maria,ai_techniques).
If we want to find out if there is anyone whom Peter likes, we add to the program the negation of this statement, i.e. ‘Peter likes nobody’ or :-likes(peter,N); this clause is called a query or a goal. We then try to refute this query by finding an inconsistency by means of resolution. A refutation proof is given in Figure 2.3. In this figure, which is called a proof tree, two clauses on a row are input clauses for a resolution step, and they are connected by lines to their resolvent, which is then again an input clause for a resolution step, together with another program clause. The mgu’s are also shown. Since the empty clause is derived, the query is indeed refuted, but only under the substitution { N → maria }, which constitutes the answer to the query.
Figure 2.3 A refutation proof which finds someone whom Peter likes.#
In general, a query can have several answers. For instance, suppose that Peter does not only like his students, but also the people his students like (and the people those people like, and …):
likes(peter,S):-student_of(S,peter).
likes(peter,Y):-likes(peter,X),likes(X,Y).
likes(maria,paul).
student_of(S,T):-follows(S,C),teaches(T,C).
teaches(peter,ai_techniques).
follows(maria,ai_techniques).
The query
?-likes(peter,N) will now have two answers.
Exercise 2.8 #
Draw the proof tree for the answer { N → paul }.
Meta-theory#
As with propositional resolution, relational resolution is sound (i.e. it always produces logical consequences of the input clauses), refutation complete (i.e. it always detects an inconsistency in a set of clauses), but not complete (i.e. it does not always generate every logical consequence of the input clauses). An important characteristic of relational clausal logic is that the Herbrand universe (the set of individuals we can reason about) is always finite. Consequently, models are finite as well, and there are a finite number of different models for any program. This means that, in principle, we could answer the question ‘is \(C\) a logical consequence of \(P\)?’ by enumerating all the models of \(P\), and checking whether they are also models of \(C\). The finiteness of the Herbrand universe will ensure that this procedure always terminates. This demonstrates that relational clausal logic is decidable, and therefore it is (in principle) possible to prevent resolution from looping if no more answers can be found. As we will see in the next section, this does not hold for full clausal logic.
Tip
constant(peter).
constant(maria).
% rel_atom(A,L) <- A is a relational atom with arguments L
rel_atom(likes(X,Y),[X,Y]).
rel_atom(student_of(X,Y),[X,Y]).
% Constants are the ground terms in relational clausal logic
ground_term(T):-
constant(T).
ground_terms([]).
ground_terms([T|Ts]):-
ground_term(T),
ground_terms(Ts).
% An atom is ground if its arguments are ground terms
ground_atom(A):-
rel_atom(A,Args),
ground_terms(Args).