Predicate Logic

Lecture Module 12
 Limitation of PL
● The facts like:
− “peter is a man”, “paul is a man”, “john is a man” can be
symbolized by P, Q and R, respectively in PL.
− We can not draw any conclusions about similarities between
P, Q and R.
● Better representations of these facts can be
● Further, the sentences like “All men are mortal” can
not be represented in PL.
− MAN(peter), MAN(paul) and MAN(john).
− Similarity between these facts that they are all man can be
easily derived.
● In Predicate Logic (logical extension of PL) such
sentences can be easily represented.
− The limitations of propositional logic are removed to some
extent.
 Predicate Logic
● It has three more logical notions as compared to PL.
−Terms, Predicates and
− Quantifiers
● Term
− a constant (single individual or concept i.e.,5, john etc.),
− a variable that stands for different individuals
− n-place function f(t1, …, tn) where t1, …, tn are terms. A
function is a mapping that maps n terms to a term.
● Predicate
− a relation that maps n terms to a truth value true (T) or false (F).
● Quantifiers
− Universal or existential quantifiers i.e.  and  used in
conjunction with variables.
 Examples
● “x loves y” is represented as LOVE(x, y) which maps it
to true or false when x and y get instantiated to actual
values.
● “john’s father loves john” is represented as
LOVE(father(john), john).
− Here father is a function that maps john to his father.
● x is greater than y is represented in predicate calculus
as GT(x, y).
● It is defined as follows:
GT( x, y) = T , if x  y
= F , otherwise
● Symbols like GT and LOVE are called predicates
− Predicates two terms and map to T or F depending upon the
values of their terms.
Examples – Cont..

● Translate the sentence "Every man is mortal"

into Predicate formula.
● Representation of statement in predicate form
− “x is a man” and “MAN(x),
− x is mortal” by MORTAL(x)
● Every man is mortal :
(x) (MAN(x) → MORTAL(x))
 First Order Predicate Logic (FOPL)
● Inference rules are added to Predicate Calculus.
● In First Order Predicate Logic (FOPL), quantification is
over variables.
− Higher order Predicate Logic is one if quantification is on
functions or predicates.
● Using inference rules one can derive new formula
using the existing ones.
● Interpretations of Formulae in FOPL
− In PL, an interpretation is simply an assignment of truth values
to the atoms.
− In FOPL, there are variables, so we have to do more than that.
− An interpretation I for a formula  in FOPL consists of a non
empty domain D and an assignment of values to each
constant, function symbol and predicate symbol.
 Cont…
● A formula  is said to be consistent (satisfiable) if
and only if there exists an interpretation I such that
I[] = T.
− Alternatively we say that I is a model of  or I satisfies .
● A formula  is said to be inconsistent
(unsatisfiable) if and only if  no interpretation that
satisfies  or there exists no model for .
● A formula  is valid if and only if for every
interpretation I, I[] = T.
● A formula  is a logical consequence of a set of
formulae {1, 2, ..., n } if and only if
− for every interpretation I, if I[1  …  n ] = T, then
I[] = T.
 Prenex Normal Form

● In FOPL, there are infinite number of domains and

consequently infinite number of interpretations of a
formula.
● Therefore, unlike PL, it is not possible to verify a
validity and inconsistency of a formula by evaluating
it under all possible interpretations.
● We will discuss the formalism for verifying
inconsistency and validity in FOPL.
● In FOPL, there is also a third type of normal form
called Prenex Normal Form.
 Contd..

● A closed formula  of FOL is said to be in Prenex

Normal Form (PNF) if and only if  is represented as

(q1 x1) (q2 x2) … (qn xn) (M),

where, qk , (1  k  n ) quant ( or ) and
M is a formula free from quantifiers.

● A list of quantifiers [(q1 x1) … (qn xn)] is called prefix

and M is called the matrix of a formula . Here M is
represented in CNF.
Transformation of Formula into PNF
● A formula can be easily transformed into PNF
using various equivalence laws.
● Following conventions are used:

−  [x] → a formula , which contains a variable x.

−  → a formula without a variable x.
− q → Quantifier ( or  ).
Equivalence Laws

● In addition to the equivalence laws given for

PL, following equivalence laws FOPL
available.

− (q x)  [x] V   (q x) ( [x] V  )
−  V (q x)  [x]  (q x) ( V  [x])
− (q x)  [x]    (q x) ( [x]   )
−   (q x)  [x]  (q x) (   [x])
− ~((x)  [x])  (x) (~ [x])
− ~((x)  [x])  (x) (~ [x])
 Skolemisation (Standard Form)

● Prenex normal form of a formula is further

transformed into special form called Skolemisation
or Standard Form.
● This form is used in resolution of clauses.
● The process of eliminating existential quantifiers and
replacing the corresponding variable by a constant
or a function is called skolemisation.
● A constant or a function is called skolem constant or
function.
 Conversion of PNF to its Standard Form

● Scan prefix from left to right.

● If q1 is the first existential quantifier then
− choose a new constant c D &  Matrix. Replace all
occurrence of x1 appearing in Matrix by c and delete
(q1 x1) from the prefix to obtain new prefix and matrix.
● If qr is an existential quantifier and q1….qr-1 are
universal quantifiers appearing before qr , then
− choose a new (r-1) place function symbol 'f ' D & 
Matrix. Replace all occurrence of xr in Matrix by f(x1,
…, xr-1 ) and remove (qr xr).
● Repeat the process till all existential quantifiers are
removed from matrix.
 Cont…
• Any formula  in FOPL can be transformed into its standard form.
• Matrix of standard formula is in CNF and prefix is free from
existential quantifiers.
• Formula in standard form is expressed as:
(x1)… (xn) (C1 … Ck),
where Ck ,(1 k m) is formula in disjunctive normal form.
• Since all the variables in prefix are universally quantified, we omit
prefix part from the standard form for the sake of convenience
and write standard form as (C1 … Ck).
• The standard form of any formula is of the form (C1 … Ck),
where each Ci , (1  i  m) is a clause.
• A clause Ci is a closed formula of the form (L1V … V Lm), where
each Li is a literal with all the variables occurring in L1, …, Lm
being universally quantified.
Cont…

• Let S = { C1, … ,Ck } be a set of clauses that

represents a standard form of a formula .
− S is said to be unsatisfiable (inconsistent) if and only if
there  no interpretation that satisfies all the clauses of
S simultaneously.
− A formula  is unsatisfiable (inconsistent) if and only if
its corresponding set S is unsatisfiable.
− S is said to be satisfiable (consistent) if and only if
each clause is consistent i.e.,  an interpretation that
satisfies all the clauses of S simultaneously.
• Alternatively, an interpretation I models S if and only
if I models each clause of S.
Resolution Refutation in Predicate Logic

● Resolution method is used to test unsatisfiability of a

set S of clauses in Predicate Logic.
● It is an extension of resolution method for PL.
● The resolution principle basically checks whether
empty clause is contained or derived from S.
● Resolution for the clauses containing no variables is
very simple and is similar to PL.
● It becomes complicated when clauses contain
variables.
● In such case, two complementary literals are
resolved after proper substitutions so that both the
literals have same arguments.
Example
● Consider two clauses C1 and C2 as follows:
C1 = P(x) V Q(x)
C2 = ~ P(f(x)) V R(x)
● Substitute 'f(a)' for 'x' in C1 and 'a' for 'x' in C2 , where 'a' is a
new constant from the domain, then
C3 = P(f(a)) V Q(f(a))
C4 = ~ P(f(a)) V R(a)
● Resolvent C of C3 and C4 is [Q(f(a)) V R(a)]
− Here C3 and C4 do not have variables. They are called
ground instances of C 1 and C2 .
● In general, if we substitute 'f(x)' for 'x' in C1 , then
C'1 = P(f(x)) V Q(f(x))
● Resolvent C' of C'1 and C2 is [Q(f(x)) V R(x)]
● We notice that C is an instance of C' .
Theorems
● Logical Consequence: L is a logical consequence of
S iff {S ~L} = { C1,,… , Cn , ~ L} is unsatisfiable.
− A deduction of an empty clause from a set S of
clauses is called a resolution refutation of S.
● Soundness and completeness of resolution:
There is a resolution refutation of S if and only if S is
unsatisfiable (inconsistent).
● L is a logical consequence of S if and only if there is
a resolution refutation of S  {~L}.
● We can summarize that in order to show L to be a
logical consequence the of set of formulae {1,…,n },
use the procedure given on next slide.
Procedure
• Obtain a set S of all the clauses.
• Show that a set S  { ~ L} is unsatisfiable i.e.,
− the set S  { ~ L} contains either empty clause or empty
clause can be derived in finite steps using resolution
method.
− If so, then report 'Yes' and conclude that L is a logical
consequence of S and subsequently of formulae 1, …, n
otherwise report 'No'.
• Resolution refutation algorithm finds a contradiction if
one exists, if clauses to resolve at each step are
chosen systematically.
• There exist various strategies for making the right
choice that can speed up the process considerably.
Useful Tips
• Initially choose a clause from the negated goal clauses as one
of the parents to be resolved.
− This corresponds to intuition that the contradiction we are looking
for must be because of the formula to be proved .
• Choose a resolvent and some existing clause if both contain
complementary literals.
• If such clauses do not exists, then resolve any pairs of clauses
that contain complementary literals.
• Whenever possible, resolve with the clauses with single literal.
− Such resolution generate new clauses with fewer literals than the
larger of their parent clauses and thus probably algorithm
terminates faster.
• Eliminate tautologies and clauses that are subsumed by other
clauses as soon as they are generated.
 Logic Programming

• Logic programming is based on FOPL.

• Clause in logic programming is special form of
FOPL formula.
• Program in logic programming is a collection of
clauses.
• Queries are solved using resolution principle.
• A clause in logic programming is represented in a
clausal notation as
A1, …, Ak  B1,…, Bt ,
where Aj are positive literals and Bk are negative literals.
Conversion of a Clause into Clausal Notation

● A clause in FOPL is a closed formula of the form,

L 1V … V L m
where each Lk , (1  k  n) is a literal and all the variables
occurring in L1, …, Lm are universally quantified.
● Separate positive and negative literals in the clause
as follows:
(L1V … V Lm)
 (A1 V … VAk V ~ B1 V …V~ Bt),
where m = k + t, Aj, (1  j  k) are positive literals
and Bj , (1  j  t) are negative literals
 Cont…

(L1V … V Lm)  (A1 V … VAk V ~ B1 V …V~ Bt),

 (A1 V … VAk ) V ~ (B1  …  Bt)
 (B1  …  Bt) → (A1 V … VAk )
{since P → Q  ~ P V Q}
● Clausal notation is written in the form :
(A1V … VAk )  (B1  …  Bt) OR A1, …, Ak  B1,…, Bt .
Here Aj , (1  j  k) are positive literals and Bi , (1  i  t) are negative literals.
● Interpretations of A  B and B → A are same.
● In clausal notation, all variables are assumed to be
universally quantified.
− Bi , (1  i  t) (negative literals) are called antecedents and A j ,
(1  j  k) (positive literals) are called consequents.
− Commas in antecedent and consequent denote conjunction
and disjunction respectively.
 Cont…
• Applying the results of FOPL to the logic programs,
− a goal G with respect to a program P (finite set of clauses) is
solved by showing that the set of clauses P  { ~ G} is
unsatisfiable or there is a resolution refutation of P  { ~ G}.
• If so, then G is logical consequence of a program P.
• There are three basic statements. These are special
forms of clauses.
− facts,
− rules and
− queries.
 Example
● Consider the following logic program.
GRANDFATHER (x, y)  FATHER (x, z) , PARENT (z, y)
PARENT (x, y)  FATHER (x, y)
PARENT (x, y)  MOTHER (x, y)
FATHER ( abraham, robert) 
FATHER ( robert, mike) 
● In FOL above program is represented as a set of
clauses as:
S={ GRANDFATHER (x, y) V ~FATHER (x, z) V ~ PARENT (z, y),
PARENT(x, y) V ~ FATHER (x, y),
PARENT(x, y) V ~ MOTHER (x, y),
FATHER ( abraham, robert),
FATHER ( robert, mike)
}
Example
● Let us number the clauses of S as follows:
i. GRANDFATHER(x, y) V ~FATHER(x, z) V ~PARENT(z, y)
ii. PARENT(x, y) V ~ FATHER (x, y)
iii. PARENT(x, y) V ~ MOTHER (x, y),
iv. FATHER ( abraham, robert)
v. FATHER ( robert, mike)
● Simple queries :
− Ground Query
Query:“Is abraham a grandfather of mike ?"
Example – Cont…

● Ground Query “Is abraham a grandfather of mike ?"

 GRANDFATHER (abraham, mike).
● In FOPL, ~GRANDFATHER(abraham, mike) is
negation of goal { GRANDFATHER (abraham, mike).
● Include {~goal} in the set S and show using
resolution refutation that S  {~ goal} is unsatisfiable
in order to conclude the goal.
● Let ~ goal is numbered as ( vi) in continuation of first
five clauses of S listed above.
vi. ~ GRANDFATHER (abraham, mike)
● Resolution tree is given on next slide:
 Resolution Tree

(i) ( vi )
{x / abraham, y / mike}

( iv) ~ FATHER(abraham, z) V ~PARENT(z, mike)

{z / robert}

~ PARENT (robert, mike) ( ii)

~ FATHER (robert, mike) (v)

Answer: Yes
 Different Type of Queries
● Non ground queries
Query:“Does there exist x such that x is a father of
robert ?” {Who is father of robert?}
 FATHER (x, robert).
Query: “Does there exist x such that abraham is a
father of x?" {abraham is father of whom?}
 FATHER (abraham, x).
Query: “Do there exist x and y such that x is a father of
y?" { who is father of whom?}
 FATHER (x, y).