2.5. The relation between clausal logic and Predicate Logic#
Clausal logic is a formalism especially suited for automated reasoning. However, the form of logic usually presented in courses on Symbolic Logic is (first-order) Predicate Logic. Predicate logic is more expressive in the sense that statements expressed in Predicate Logic often result in shorter formulas than would result if they were expressed in clausal logic. This is due to the larger vocabulary and less restrictive syntax of Predicate Logic, which includes quantifiers (‘for all’ (\(\forall\)) and ‘there exists’ (\(\exists\))), and various logical connectives (conjunction (\(\land\)), disjunction (\(\lor\)), negation (\(\neg\)), implication (\(\rightarrow\)), and equivalence (\(\leftrightarrow\))) which may occur anywhere within a formula.
The order of logics#
A logic with propositions (statements that can be either true or false) as basic building blocks is called a propositional logic; a logic built on predicates is called a Predicate Logic. Since propositions can be viewed as nullary predicates (i.e. predicates without arguments), any propositional logic is also a Predicate Logic.
A logic may or may not have variables for its basic building blocks. If it does not include such variables, both the logic and its building blocks are called first-order; this is the normal case. Thus, in first-order Predicate Logic, there are no predicate variables, but only first-order predicates.
Otherwise, an \(n^{\text{th}}\) order logic has variables (and thus quantifiers) for its \((n - 1)^{\text{th}}\) order building blocks. For instance, the statement
defining two individuals to be equal if they have the same properties, is a statement from second-order Predicate Logic, because P is a variable ranging over first-order predicates.
Another example of a statement from second-order Predicate Logic is
This statement defines the transitivity of binary relations. Since transitive has a second-order variable as argument, it is called a second-order predicate.
Being syntactically quite different, clausal logic and Predicate Logic are semantically equivalent in the following sense: every set of clauses is, after minor modifications, a formula in Predicate Logic, and conversely, every formula in Predicate Logic can be rewritten to an ‘almost’ equivalent set of clauses. Why then bother about Predicate Logic at all in this book? The main reason is that in Chapter 8, we will discuss an alternative semantics of logic programs, defined in terms of Predicate Logic. In this section, we will illustrate the semantic equivalence of clausal logic and Predicate Logic. We will assume a basic knowledge of the syntax and semantics of Predicate Logic.
We start with the propositional case. Any clause like
married;bachelor:-man,adult.
can be rewritten by reversing head and body and replacing the ‘:-’ sign by an implication ‘\(\rightarrow\)’, replacing ‘,’ by a conjunction ‘\(\land\)’, and replacing ‘;’ by a disjunction ‘\(\lor\)’, which yields
By using the logical laws \(A \rightarrow B \equiv \neg A \lor B\) and \(\neg (C \land D) \equiv \neg C \lor \neg D\), this can be rewritten into the logically equivalent formula
which, by the way, clearly demonstrates the origin of the terms negative literal and positive literal!
A set of clauses can be rewritten by rewriting each clause separately, and combining the results into a single conjunction, e.g.
married;bachelor:-man,adult.
has_wife:-man,married.
becomes
Formulas like these, i.e. conjunctions of disjunctions of atoms and negated atoms, are said to be in conjunctive normal form (CNF).
The term ‘normal form’ here indicates that every formula of Predicate Logic can be rewritten into a unique equivalent formula in conjunctive normal form, and therefore to a unique equivalent set of clauses. For instance, the formula
can be rewritten into CNF as (replace \(A \rightarrow B\) by \(\neg A \lor B\), push negations inside by means of De Morgan’s laws: \( \neg (C \land D) \equiv \neg C \lor \neg D\) and \( \neg (C \lor D) \equiv \neg C \land \neg D\), and distribute \( \land \) over \( \lor \) by means of \((A \land B) \lor C \equiv (A \lor C) \land (B \lor C)\)):
and hence into clausal form as
adult:-married.
man;woman:-married.
child;adult.
child;man;woman.
Using a normal form has the advantage that the language contains no redundancy: formulas are only equivalent if they are identical (up to the order of the subformulas). A slight disadvantage is that normal forms are often longer and less understandable (the same objection can be made against resolution proofs).
For rewriting clauses from full clausal logic to Predicate Logic, we use the same rewrite rules as for propositional clauses. Additionally, we have to add universal quantifiers for every variable in the clause. For example, the clause
reachable(X,Y,route(Z,R)):-
connected(X,Z,L),
reachable(Z,Y,R).
becomes
The reverse process of rewriting a formula of Predicate Logic into an equivalent set of clauses is somewhat complicated if existential quantifiers are involved (the exact procedure is given as a Prolog program in Section 11.1 (appendix)). An existential quantifier allows us to reason about individuals without naming them. For example, the statement ‘everybody loves somebody’ is represented by the Predicate Logic formula
Recall that we translated this same statement into clausal logic as
loves(X,person_loved_by(X)).
These two formulas are not logically equivalent! That is, the Predicate Logic formula has models like {loves(paul,anna)} which are not models of the clause. The reason for this is, that in clausal logic we are forced to introduce abstract names, while in Predicate Logic we are not (we use existential quantification instead). On the other hand, every model of the Predicate Logic formula, if not a model of the clause, can always be converted to a model of the clause, like {loves(paul,person_loved_by(paul))}. Thus, we have that the formula has a model if and only if the clause has a model (but not necessarily the same model).
So, existential quantifiers are replaced by functors. The arguments of the functor are given by the universal quantifiers in whose scope the existential quantifier occurs. In the above example, \(\exists \texttt{Y}\) occurs within the scope of \(\forall \texttt{X}\), so we replace Y everywhere in the formula by person_loved_by(X), where person_loved_by should be a new functor, not occurring anywhere else in the clause (or in any other clause). This new functor is called a Skolem functor, and the whole process is called Skolemisation. Note that, if the existential quantifier does not occur inside the scope of a universal quantifier, the Skolem functor does not get any arguments, i.e. it becomes a Skolem constant. For example, the formula
(‘somebody loves everybody’) is translated to the clause
loves(someone_who_loves_everybody,X).
Finally, we illustrate the whole process of converting from Predicate Logic to clausal logic by means of an example. Consider the sentence ‘Everyone has a mother, but not every woman has a child’. In Predicate Logic, this can be represented as
First, we push the negation inside by means of the equivalences \(\neg \forall X : F \equiv \exists X : \neg F\) and \(\neg \exists Y : G \equiv \forall Y : \neg G \), and the previously given propositional equivalences, giving
The existential quantifiers are Skolemised: X is replaced by mother(Y), because it is in the scope of the universal quantifier \(\forall \texttt{Y}\). \(\texttt{Z}\), however, is not in the scope of a universal quantifier; therefore it is replaced by a Skolem constant childless_woman. The universal quantifiers can now be dropped:
This formula is already in CNF, so we obtain the following set of clauses:
mother_of(mother(Y),Y).
woman(childless_woman).
:- mother_of(childless_woman,W).
Translate to clausal logic:
\( \forall \texttt{X} \exists \texttt{Y} : \texttt{mouse(X)} \rightarrow \texttt{tail_of(Y,X)} \);
\( \forall \texttt{X} \exists \texttt{Y} : \texttt{loves(X,Y)} \land ( \forall \texttt{Z} : \texttt{loves(Y,Z)} ) \);
\( \forall \texttt{X} \forall \texttt{Y} \exists \texttt{Z} : \texttt{number(X)} \land \texttt{number(Y)} \rightarrow \texttt{maximum(X,Y,Z)} \).