UNIT - II

Syllabus: Logic concepts: Introduction, propositional calculus, propositional logic,

natural deduction system, axiomatic system, semantic tableau system in propositional
logic, resolution refutation in propositional logic, predicate logic.
Introduction
 One particular way of representing facts is the language of logic.
 The logical formalism is appealing because it immediately suggests a powerful way
of deriving new knowledge from old called as “mathematical deduction”.
 In this formalism, we can conclude that a new statement is true by proving that it
follows from the statements that are already known.
 The way of demonstrating the truth of an already believed proposition can be
extended to include deduction as a way of deriving answers to questions and solutions
to problem.
We use the following standard logic symbols:
 (Implication)
 ¬ (Not)
 Λ (And)
 V (Or)
 ∃ (there exists) ∀ (For All)
Propositional logic
 Propositional logic (PL) is the simplest form of logic where all the statements are
made by propositions. A proposition is a declarative statement which is either true or
false. It is a technique of knowledge representation in logical and mathematical form.
 Propositional logic is also called Boolean logic as it works on 0 and 1.
 In propositional logic, we use symbolic variables to represent the logic, and we can
use any symbol for a representing a proposition, such A, B, C, P, Q, R, etc.
 Propositions can be either true or false, but it cannot be both
 Propositional logic consists of an object, relations or function, and logical
connectives.
 These connectives are also called logical operators.
 The propositions and connectives are the basic elements of the propositional logic.
 Connectives can be said as a logical operator which connects two sentences.
 A proposition formula which is always true is called tautology, and it is also called a
valid sentence.
 A proposition formula which is always false is called Contradiction.
 A proposition formula which has both true and false values is called Contingency
 Statements which are questions, commands, or opinions are not propositions such as
"Where is Rohini", "How are you", "What is your name", are not propositions.
 The syntax of propositional logic defines the allowable sentences for the knowledge

Dr. Ram Prasad Reddy Sadi Page 1

 UNIT - II

representation.
 There are two types of Propositions:
o Atomic Propositions: Atomic propositions are the simple propositions. It
consists of a single proposition symbol. These are the sentences which must be
either true or false.
Examples:
a) 2+2 is 4, it is an atomic proposition as it is a true fact.
b) "The Sun is cold" is also a proposition as it is a false fact.
o Compound propositions: Compound propositions are constructed by
combining simpler or atomic propositions, using parenthesis and logical
connectives.
Examples:
a) "It is raining today, and street is wet."
b) "Ankit is a doctor, and his clinic is in Mumbai."
 Logical connectives are used to connect two simpler propositions or representing a
sentence logically. We can create compound propositions with the help of logical
connectives. There are mainly five connectives, which are given as follows:
o Negation: A sentence such as ¬ P is called negation of P. A literal can be
either Positive literal or negative literal.
o Conjunction: A sentence which has ∧ connective such as, P ∧ Q is called a
conjunction.
Example: Rohan is intelligent and hardworking. It can be written as,
P= Rohan is intelligent,
Q= Rohan is hardworking. → P∧ Q.
o Disjunction: A sentence which has ∨ connective, such as P ∨ Q. is called
disjunction, where P and Q are the propositions
Example: "Ritika is a doctor or Engineer"
Here P= Ritika is Doctor.
Q= Ritika is Doctor, so we can write it as P ∨ Q.
o Implication: A sentence such as P → Q, is called an implication. Implications
are also known as if-then rules.
Example: If it is raining, then the street is wet. Let P= It is raining and
Q= Street is wet, so it is represented as: P → Q
o Biconditional: A sentence such as P⇔ Q is a Biconditional sentence,
Example: If I am breathing, then I am alive
P= I am breathing,
Q= I am alive, it can be represented as P ⇔ Q.

Dr. Ram Prasad Reddy Sadi Page 2

 UNIT - II

Truth Table:

P Q ¬Q P∧Q P∨Q P→Q P⇔ Q

T T F T T T T

T F T F T F F

F T F F T T F

F F T F F T T

Limitations of Propositional logic:

 We cannot represent relations like ALL, some, or none with propositional logic.
Example: All the girls are intelligent. Some apples are sweet.
 Propositional logic has limited expressive power.
 In propositional logic, we cannot describe statements in terms of their properties or
logical relationships.
Natural Deduction:
 It mimics the pattern of natural reasoning
 It is based on a set of deductive inference rules
 Assuming that A1, A2, . . ., Ak, 1 ≤ k ≤ n, are a set of items and αj , where 1 ≤ j ≤ m,
and β are well formed formulae, the inference rules may be stated as shown in the
following NDS rules table
NDS Inference Rules

Rule Name Symbol Rule

Introducing Ʌ (I : Ʌ) If A1, . . ., An then A1Ʌ . . . Ʌ An

Eliminating Ʌ (E : Ʌ) If A1Ʌ . . . Ʌ An then Ai (1 ≤ i ≤ n)

Introducing V (I : V) If any Ai (1 ≤ i ≤ n) then A1V . . . V An

Eliminating V (E : V) If A1V . . . V An, A1→A, . . . An→A then A

Introducing → (I : →) If from A1, . . ., An infer B is proved then then A1Ʌ . .

. Ʌ An →B is proved

Eliminating → (E : →) If A1→A , A1 , then A (Modus Ponen Rule)

Introducing ↔ (I : ↔) If A1→A2 , A2 →A1 then A1↔A2

Eliminating ↔ (E : ↔) If A1↔A2 then A1→A2 , A2 →A1

Introducing ~ (I : ~) If from A infer A1 Ʌ ~A1 is proved then ~A is proved

Dr. Ram Prasad Reddy Sadi Page 3

 UNIT - II

Eliminating ~ (E : ~) If from ~A infer A1 Ʌ ~A1 is proved then A is proved

 Deduction Theorem: To prove a formula α1 Ʌ . . . Ʌ αn → β , it is sufficient to

prove a theorem from α1 , . . . , αn → β . Conversely, if α1 Ʌ . . . Ʌ αn → β is proved
then the theorem from α1 , . . . , αn infer β is assumed to be proved
Axiomatic System
 It is based on a set of three axioms and one rule of deduction
 It is minimal in structure but powerful as the truth table and NDS approaches
 In axiomatic system, the proofs of the theorems are often difficult and require a guess
in selection of appropriate axiom(s)
 In this system, only two logical operators not(~) and implies(→) are allowed to form
a formula, other logical operators V, Ʌ, and ↔ can be easily expressed in terms of ~
and → using equivalence laws
 For example: A Ʌ B ≅ ~(~A V ~B) ≅ ~(A → ~B) A V B ≅ ~A → B A ↔ B ≅ (A →
B) Ʌ (B → A) ≅ ~[(A → B) → ~(B → A)]
 In axiomatic system, there are three axioms, which are always true (or valid), and one
rule called modus ponen (MP). Here α, β and γ are well-formed formulae of the
axiomatic system. The three axioms and the rule are stated as follows:
o Axiom 1 : α → (β → α)
o Axiom 2 : [α → (β → γ) ] → [(α → β) → (α → γ)]
o Axiom 3 : (~α → ~β) → (β → α)
o Modus Ponen Rule Hypothesis : α → β and α ; Consequent : β Interpretation
of Modus Ponen Rule : Given that α → β and α are hypotheses , β is inferred
as a consequent
 Let Σ = {α1, . . ., αn} be a set of hypotheses. The formula α is defined to be a
deductive consequence of Σ if either α is an axiom or a hypothesis or is derived from
αj , 1≤ j≤ n, using Modus Ponen inference rule. It is represented as {α1, . . ., αn} ˫ α or
more formally as Σ ˫ α.
 If Σ is an empty set and α is deduced, then we can write ˫ α. In this case, α is deduced
from axioms only and no hypotheses are used. In such situations, α is said to be a
theorem.
 Deduction Theorem: Given that Σ is a set of hypotheses and α and β are well formed
formulae. If β is proved from {Σ U α} , then according to the deduction theorem, (α
→ β) is proved from Σ. Alternatively, we can write {Σ U α}˫ β implies Σ ˫ (α → β)
Converse of Deduction Theorem : The converse of deduction theorem can be stated
as: Given Σ ˫ (α → β) , then {Σ U α}˫ β is proved. Points to remember while dealing
with an axiomatic system:
 If α is given, then we can easily prove β → α for any well-formed formulae α and β
 If α → β is to be proved, then include α in the set of hypotheses Σ and derive β from
the set {Σ U α} . Then by using deduction theorem, we can conclude that α → β

Dr. Ram Prasad Reddy Sadi Page 4

 UNIT - II

Semantic Tableau in propositional logic

 Semantic tableau is designed to make semantic reasoning fully systematic and to
generate decisions automatically as to whether sequent is valid or not.
 The idea of a tableau is to take a set of formulae with labels saying which are true and
which false, and to process them by analyzing them into their sub formulae,
transferring the labels to those in accordance with the semantics of the various
connectives, until either the analysis is complete or a contradiction results.
 Each node of the tableau is characterized by a set of labeled formulae, and if it has
successor nodes, these result by analysis of some formula in the set into its principal
sub formulae. For example, suppose there is a conjunction A ∧ B in the set with the
label t (i.e. true). For a conjunction to be true is exactly for both of its conjuncts to be
true, so we can choose to extend the tableau by analyzing the conjunction, in which
case the successor node will have the two formulae A and B each with label t in place
of the conjunction. On the other hand, if we choose to analyze a disjunction A ∨ B
also with the label t, there will be no unique successor node, since there is nothing to
say which disjunct should be the true one. Instead, there will be two successors, one
with A labeled t in place of the disjunction, and the other with B.
 The rules for extending tableaux to analyze negations, conjunctions and disjunctions:

 A set of labeled formulae including the one above the line may be developed by
replacing that formula with the one or more formulae below the line. A vertical bar
separating two sets below the line, indicates that there are two successor nodes, so the
branch of the tableau splits into two at that point.
 A contradiction in a tableau branch causes that branch to die: it gets closed off and no
more growth happens from its tip. If every branch dies, the tree dies; in that case we
know there was no way the tested formulas could all have had the truth values they
were initially supposed to have.
 If, on the other hand, we get to a state in which every subformula has been processed
in every branch in which it occurs and some branch is left alive or "open", we have
found an interpretation on which all of the original formulas are true. Conventionally
we mark a dead or "closed" branch by writing a cross under it.

Dr. Ram Prasad Reddy Sadi Page 5

 UNIT - II

Resolution Refutation Method

 Another simple method that can be used in propositional logic to prove a formula or
derive a goal from a given set of clauses by contradiction is the resolution refutation
method.
 The term clause is used to denote special formula containing the boolean operators ~
and V
 Resolution Refutation is the most favoured method for developing computer-based

Dr. Ram Prasad Reddy Sadi Page 6

 UNIT - II

systems that can be used to prove theorems automatically

 It uses a single inference rule, which is known as resolution based on modus ponen
inference rule
 It is more efficient in comparison to NDS and Axiomatic System because in this case
we do not need to guess which rule or axiom to apply in development of proofs
 Negation of the goal to be proved is added to the given set of clauses and using the
resolution principle, it is shown that there is a refutation in the new set
Conversion of a Formula into a set of clauses
 In PC, there are two normal forms: DNF and CNF. A formula is said to be in its
normal form if it is constructed using only natural connectives {~, Ʌ, V }
 Formally, a clause is defined as a formula of the form ( L1 V . . . V Lm). Therefore if
a given formula is converted to its equivalent CNF as (C1 Ʌ. . . Ʌ Cn ) then the set of
clauses is a set of each conjunct of CNF i.e. {C1 . . . Cn }
 For eg. { A V B, ~A V D, C V ~ B} represent a set of clauses A V B, ~A V D, C V ~
B
Conversion of a Formula to its CNF
 Any formula in PC can be easily transformed into its equivalent CNF representation
by using the following equivalence laws:
 Eliminate double negation by using ~(~A) ≅ A
 Use DeMorgan’s Laws to push (~) negation immediately before the atomic formula
~( A Ʌ B) ≅ ~ A V ~ B ~( A V B) ≅ ~ A Ʌ ~ B
 Use distributive laws to get CNF A V ( B Ʌ C) ≅ (A V B) Ʌ ( A V C)
 Eliminate → and ↔ by using the following equivalence laws: A → B ≅ ~ A V B A
↔ B ≅ (A → B) Ʌ (B → A)
Resolution of clauses
 Two clauses can be resolved by eliminating complementary pair of literals , if any,
from both, a new clause is constructed by disjunction of the remaining literals in both
the clauses
 If two clauses C1 and C2 contain a complementary pair of literals { L, ~L } then these
clauses may be resolved together by deleting L from C1 and ~L from C2 and
constructing a new clause by the disjunction of remaining literals in C1 and C2. This
new clause is called resolvent of C1 and C2. The clauses C1 and C2 are called parent
clauses
Key Points:
 If C is a resolvent of two clauses C1 and C2 then C is called a logical consequence of
the set of the clauses {C1 , C2} . This is known as Resolution Principle
 If a contradiction(or an empty clause) is derived from a set S of clauses using
resolution then S is said to be unsatisfiable. Derivation of contradiction for a set S by
resolution method is called a resolution refutation of S
 A clause C is said to be a logical consequence of S if C is derived from S
 Alternatively, using the resolution refutation concept, a clause C is defined to be a

Dr. Ram Prasad Reddy Sadi Page 7

 UNIT - II

logical consequence of S if and only if the set S’ = S ⋃ {~C} is unsatisfiable, that is, a
contradiction (or an empty clause) is deduced from the set S’, assuming that initially
the set S is satisfiable
Representing Simple Facts in Logic
 Propositional logic is appealing because it is simple to deal with and a decision
procedure for it exists.
 We can easily represent real-world facts as logical propositions written as well
formed formulas (wff’s) in Propositional logic.
 Some Simple Facts in Propositional logic:
o It is raining
 RAINING
o It is sunny
 SUNNY
o It is windy
 WINDY
o If it is raining, then it is not sunny.
 RAINING ¬SUNNY
 Suppose we want to represent the fact stated by the sentence: Socrates is a man
We could write SOCRATESMAN. It is represented as:
MAN (SOCRATES)
 Now the structure of the representation reflects the structure of the knowledge itself.
But to do that, we need to be able to use “predicates” applied to arguments.
 To represent the following sentence: All men are mortal
We can’t represent this as: MORTALMAN
 But that fails to capture the relationship between any individual being a man and that
individual being a mortal. To do that, we need variables and quantification.
 So we use first-order predicate logic as a way of representing knowledge because it
permits representations of things that cannot be represented in propositional logic.
 In predicate logic, we can represent real-world facts as statements written as wff's.
 The major motivation for choosing to use logic is that it we use logical statements as a
way of representing knowledge, and then we have a good way of reasoning with that
knowledge.
 Determining the validity of a proposition in propositional logic is straightforward,
although it may be computationally hard.
 Before we use predicate logic as a medium for representing knowledge, we need to
check whether it also provides a good way of reasoning with the knowledge.
 It provides a way of deducing new statements from old ones.
 Unfortunately, unlike propositional logic, it does not possess a decision procedure.

Dr. Ram Prasad Reddy Sadi Page 8

 UNIT - II

 There do exist procedures that will find a proof of a proposed theorem, but first-order
predicate logic is not decidable, it is semi-decidable.
 A simple such procedure is to use the rules of inference to generate theorems from the
axioms in some orderly fashion.
 This method is not particularly efficient, however, and we will want to try to find a
better one.
Use of predicate logic
Let’s now explore the use of predicate logic as a way of representing knowledge by looking
at a following example: Consider the following set of sentences:
1. Marcus was a man.
2. Marcus was a Pompeian.
3. All Pompeians were Romans.
4. Caesar was a ruler.
5. All Romans were either loyal to Caesar or hated him.
6. Everyone is loyal to someone.
7. People only try to assassinate rulers they are not loyal to.
8. Marcus tried to assassinate Caesar.
 The facts described by these sentences can be represented as a set of wff’s in
predicate logic as follows:
1. Marcus was a man.
 man (Marcus)
This representation captures the critical fact of Marcus being a man. It fails to capture
some of the information in the English sentence, the notion of past tense.
2. Marcus was a Pompeian.
 Pompeian (Marcus)
3. All Pompeians were Romans.
 ∀(x): Pompeian(x)  Roman(x)
4. Caesar was a ruler.
 ruler (Caesar)
5. All Romans were either loyal to Caesar or hated him.
 ∀(x): Roman(x)  loyalto(x, Caesar) V hate( x , Caesar)
6. Everyone is loyal to someone.
 ∀(x) : ∃(y): loyalto(x, y)
7. People only try to assassinate rulers they are not loyal to
 ∀(x) : ∃(y):person(x) 𝖠 ruler(y) 𝖠 tryassassinate(x, y)  ¬loyalto(x, y)
8. Marcus tried to assassinate Caesar

Dr. Ram Prasad Reddy Sadi Page 9

 UNIT - II

 tryassassinate(Marcus, Caesar)
 Now suppose that we want to use these statements to answer the question:
Was Marcus loyal to Caesar?
Let's try to produce a formal proof, reasoning backward from the desired goal:
¬loyalto (Marcus, Caesar)
To prove this, let us add a fact:
 All men are people
Although we know that Marcus was a man, we do not have any way to conclude that Marcus
was a person. So, we need therepresentation of another fact to our system,
∀(x):

Representing Instance and isa Relationships

 The specific attributes instance and isa play an important role in the useful form of
reasoning, property inheritance.
 Let us represent the following facts in three ways:
1. Marcus was a man.
2. Marcus was a Pompeian.
3. All Pompeians were Romans.
4. Caesar was a ruler.

Dr. Ram Prasad Reddy Sadi Page 10

 UNIT - II

5. All Romans were either loyal to Caesar or hated him.

 Second representation: The predicate instance is a binary one, whose first argument
is an object and whose second argument is a class to which the object belongs. But
these representations do not use an explicit isa predicate.
 In subclass relationships, such as that between Pompeians and Romans, the
implication rule there states that it an object is an instance of the subclass Pompeian
then it is an instance of the superclass Roman.
 This rule is equivalent to the standard set-theoretic definition of the subclass-
superclass relationship.
 Third representation: It contains representations that use both the instance and isa
predicates explicitly.
 The use of the isa predicate simplifies the representation of sentence 3, but it
requires that one additional axiom. This additional axiom describes how an instance
relation and an isa relation can be combined to derive a new instance relation.

Representing facts in Propositional Logic:

Consider the following set of facts:
1. Marcus was a man.
2. Marcus was a Pompeian.
3. Marcus was boni in 40 A.D.
4. All men are mortal.
5. All Pompeians died when the volcano erupted in 79 AD.
6. No mortal lives longer than 150 years.

Dr. Ram Prasad Reddy Sadi Page 11

 UNIT - II

7. It is now 1991.
8. Alive means not dead.
9. If someone dies, then he is dead at all later times.
Now let's attempt to answer the question:
"Is Marcus alive?"
By proving:
¬ alive(Marcus, now)
The given facts are represented as follows:

Resolution:
 Resolution is such a procedure, which gains its efficiency from the fact that it operates
on statements that have been converted to a very convenient standard form.
 Resolution produces proofs by refutation. To prove a statement (to show that it is
valid), resolution attempts to show that the negation of the statement produces a
contradiction with the known statements (i.e.. that it is unsatisfiable).
 Resolution is a technique for proving theorems in the propositional or predicate
calculus that has been a part of AI problem-solving.
 Resolution describes a way of finding contradictions in a database of clauses with

Dr. Ram Prasad Reddy Sadi Page 12

 UNIT - II

minimum use of substitution. Resolution refutation proves a theorem by negating the

statement to be proved and adding this negated goal to the set of axioms that are
known (have been assumed) to be true.
 It then uses the resolution rule of inference to show that this leads to a contradiction.
Once the theorem prover shows that the negated goal is inconsistent with the given set
of axioms, it follows that the original goal must be consistent. This proves

 Resolution refutation proofs involve the following steps:

1. Put the premises or axioms into clause form.
2. Add the negation of what is to be proved, in clause form, to the set of axioms.
3. Resolve these clauses together, producing new clauses that logically follow
from them.
4. Produce a contradiction by generating the empty clause.
5. The substitutions used to produce the empty clause are those under which the
opposite of the negated goal is true.
Conversion to Clause Form:
Consider the following fact:
 All Romans who know Marcus either hate Caesar or think that anyone who hates
anyone is crazy.
o ∀x:[Roman(X)⋀ ∀y:∃z:hate(y,z)
thinkcrazy(x, y))]

Dr. Ram Prasad Reddy Sadi Page 13

 UNIT - II

Algorithm: Conversion to clause form:

1. Eliminate, using the fact that ab is equivalent to¬ aVb. Performing this
transformation, we get:
o ∀x:¬[Roman(X)⋀know(x,Marcus)]V[hate(x,Caesar)V(∀y:¬(∃z:hate(y,z))Vthi
nkcrazy(x,y))]
2. Reduce the scope of each ¬ to a single term, using the fact that ¬(¬P)=P and
deMorgan's laws [which say that (¬(a⋀b) = ¬aV ¬b and (¬(a V b)= ¬a⋀ ¬b) and the
standard correspondences between quantifiers:- ∀x: P(x)= ∃x: ¬P(x) and ∃x: P(x)=
∀x: ¬P(x)
o Performing this , we get:
∀x:[¬Roman(X)V¬know(x,Marcus)]V[hate(x,Caesar)V(∀y:∀z:¬hate(y,
z))V(thinkcrazy(x, y))]
3. Standardize variables so that each quantifier binds a unique variable. Since variables
are just dummy names, this process cannot affect the truth value of the wff. For
example, the formula:
o ∀x : P(x) V ∀x: Q(x) would be converted to: ∀x : P(x) V ∀y: Q(y)
4. Move all quantifiers to the left of the formula without changing their relative order.
This is possible since there is no conflict among variable names.
Performing this, we get:
o ∀x:∀y:∀z:[¬Roman(X)V¬know(x,Marcus)]V[hate(x,Caesar)V(¬hate(y,
z)Vthinkcrazy(x, y))]
 At this point, the formula is known as Prenex normal form. It consists of a prefix of
quantifiers followed by a matrix, which is quantifier-free.
5. Eliminate existential quantifiers. For example, the formula ∃y:President(y) can be
transformed into the formula:
o President(S1) where S1 is a function with no arguments that somehow
produces a value that satisfies President.
If existential quantifiers occur within the scope of universal quantifiers, then the value
that satisfies the predicate may depend on the values of the universally quantified
variables. For example:
o ∀x: ∃y: father-of(y, x)
The value of' y that satisfies father-of depends on the particular value of x, we must
generate functions with the same number of arguments as the number of universal
quantifiers in whose scope the expression occurs. So this would be transformed
into:
o ∀x: father-of(S2(x), x))
These generated functions are called Skolem Functions. Sometimes ones with no
arguments are called Skomlem constants.
6. Drop the prefix. All remaining variables are universally quantifled, so the prefix can
just be dropped and any proof procedure we use can simply assume that any variable
it sees is universally quantified.

Dr. Ram Prasad Reddy Sadi Page 14

 UNIT - II

o [¬Roman(X)V¬know(x,Marcus)]V[hate(x,Caesar)V(¬hate(y, z) V thinkcrazy
(x, y))]
7. Convert the matrix into a conjunction of disjuncts. Since there are no and's, it is only
necessary to exploit the associative property of (i.e., a⋁(b ⋁c) =(a ⋁b)⋁c and simply
remove the parentheses.
o ¬Roman(X)V¬know(x,Marcus)Vhate(x,Caesar)V (¬hate(y, z) V thinkcrazy(x,
y)
8. Create a separate clause corresponding to each conjunct. In order for a wff to be true,
all the clauses that are generated from it must be true. If we are going to be working
with several wff's, all the clauses generated by each of them can now be combined to
represent the same set of facts as were represented by the original wff's.
9. Standardize apart the variables in the set of clauses.
o (∀x:P(x)⋀Q(x))=∀x:P(x)⋀ ∀x:Q(x)
Since each clause is a separate conjunct and since all the variables are universally
quantified, there is no relationship between the variables of two clauses, even if they
were generated from the same wff.
The Basis of Resolution
 The resolution procedure is a simple iterative process: at each step two clauses,
called the parent clauses, are compared (resolved), yielding a new clause that has
been inferred from them. The new clause represents ways that the two parent clauses
interact with each other. Suppose there are two clauses in the system:
winter V summer
¬winter V cold
 Now we observe that precisely one of winter and ¬winter will be true at any point.
 If winter is true, then cold must be true to guarantee the truth of the second clause.
 If ¬winter is true, then summer must be true to guarantee the truth of the first clause.
 Thus we see that from these two clauses we can deduce:
summer V cold
 Resolution operates by taking two clauses that each contains the same literal, in this
example, winter. The literal must occur in positive form in one clause and in negative
form in the other. The resolvent is obtained by combining all of the literals of the two
parent clauses except the ones that cancel.
 If the clause that is produced is the empty clause, then a contradiction has been found.
For example. the two clauses:
Winter
¬winter will produce the empty clause.
 In predicate logic, the situation is more complicated since we must consider all
possible ways of substituting values for the variables.
The Unification Algorithm
 In predicate logic, this matching process is more complicated since the arguments of

Dr. Ram Prasad Reddy Sadi Page 15

 UNIT - II

the predicates must be considered.

 For example, man(John) and ¬man(John) is a contradiction, while man(John) and
¬man{Spot) is not.
 Thus, in order to determine contradictions, we need a matching procedure that
compares two literals and discovers whether there exists a set of substitutions that
makes them identical. The straightforward recursive procedure, called the “unification
algorithm” does this.
 Basic idea of unification: It is very simple. To attempt to unify two literals, we first
check if their initial predicate symbols are the same. If so, we can proceed. Otherwise,
there is no way they can he unified, regardless of their arguments.
 For example, the two literals:
o trytoassassinate( Marcus, Caesar) hate(Marcus, Caesar)
cannot be unified.
 If the predicate symbols match, then we must check the arguments one pair at a time.
If the first matches, we can continue with the second, and so on. To test each
argument pair, we can simply call the unification procedure recursively.
 The matching rules are simple: Different constants or predicates cannot match;
identical ones can. A variable can match another variable, any constant, or a
predicate expression with the restriction that the predicate expression must not contain
any instances of the variable being matched.
 We must find a single, consistent substitution for the entire literal, not separate ones
for each piece of it. To do this, we must take each substitution that we find and apply
it to the remainder of the literals before we continue trying to unify them.
 For example, suppose we want to unify the expressions
o P(x) and P(y)
 The two instances of P match. Next we compare x and y, and decide that if we
substitute y for x, they could match. We will write that substitution as: y/x.

 But now, if we simply continue and match x and z, we produce the substitution z/x.
But we cannot substitute both y and z for x. The problem can be solved as follows:
 What we need to do after finding the first substitution y/x is to make that substitution
throughout the literals, giving:
 Now we can attempt to unify arguments y and z, which succeeds with the substitution
z/y. The entire unification process has now succeeded with a substitution that is the
composition of the two substitutions: (z/y) (y/x).
 In general, substitutions: (a1/a2, a3/a4,....)(b1/b2, b3/b4....) means to apply all the
substitutions of the right most list, then take the result and apply all the ones of the
next list, and so forth, until all substitutions have been applied.
 The objective of the unification procedure is to discover at least one substitution that
causes two literals to match.
o For example, the literals:

Dr. Ram Prasad Reddy Sadi Page 16

 UNIT - II

hate (x, y)
hate (Marcus, z)
could be unified with any of the following substitutions:
(Marcus/x, z/y) (Marcus/x, y/z)
(Marcus/x, Caesar/y, Caesar/z) (Marcus/x, Polonius/y, Polonius/z)
 We describe a procedure Unify (Ll, L2), which returns as its value a list representing
the composition of the substitutions that were performed during the match. The empty
list, NIL, indicates that a match was found without any substitutions. The list
consisting of the single value FAIL indicates that the unification procedure failed.
Algorithm: Unify (L1, L2)
1. If L1 and L2 are both variables and constants, then:
a. If L1 and L2 are identical, then return NIL.
b. Else if L1 is a variable, then if LI occurs in L2 then return {FAIL}, else return
(L2/L1).
c. Else if L2 is a variable then if L2 occurs in L1 then return {FAIL}, else return
(LI/L2)
d. Else return {FAIL}.
2. If the initial predicate symbols in LI and L2 are not identical, then return {FAIL}.
3. If Ll and L2 have a different number of arguments, then return {FAlL}.
4. Set SUBST to NIL. (At the end of this procedure, SUBST will contain all the
substitutions used to unify L1 and L2).
5. For i1 to number of arguments in LI:
a. Call Unify with the ith argument of LI and ith argument of L2, putting result
in S.
b. If contains FAIL, then return {FAIL}.
c. If S not equal to NIL then:
i. Apply S to the remainder of both L1 and L2.
ii. SUBST= APPEND(S, SUBST).
6. Return SUBST.
Resolution in Predicate Logic
 With Unification, we now have an easy way of determining that two literals are
contradictory, if one of them can be unified with the negation of the other.
 So, for example, man(x) and ¬man(Spot) are contradictory, since man(x) and
man(Spot) can be unified, with substitution x/spot.
 In order to use resolution for expressions in the predicate logic, we use the unification
algorithm to locate pairs of literals that cancel out.
 For example, suppose we want to resolve two clauses:
man(Marcus)

Dr. Ram Prasad Reddy Sadi Page 17

 UNIT - II

¬man(x1) V mortal(x1)
The literal man(Marcus)can be unified with the literal ¬man(x1) with the substitution
Marcus/x1. we can now conclude only that mortal(Marcus) must be true.
 So the resolvent generated by clauses 1 and 2 must be mortal (Marcus), which we
get by applying me result of the unification process to the resolvent. The
resolution process can then proceed from there to discover whether mortal (Marcus)
leads to a contradiction with other available clauses.
Algorithm: Resolution in predicate logic
1. Convert all the statements of F to clause form.
2. Negate P and convert the result to clause form. Add it to the-set of clauses obtained in
1.
3. Repeat until a contradiction is found, no progress can be made, or a predetermined
amount of effort has been expended.
a. Select two clauses. Call these the parent clauses.
b. Resolve them together. The resolvent will be the disjunction of all the literals
of both parent clauses with appropriate substitutions performed and with the
following exception: If there is one pair of literals TI and ¬T2 such that one
of the parent clauses contains T1 and the other contains ¬T2 and if T1 and T2
are unifiable, then neither T1 nor T2 should appear in the resolvent. We call
T1 and T2 Complementary Literals. Use the substitution produced by the
unification to create the resolvent. If there is more than one pair of
complementary literals, only one pair should be omitted from the resolvent.
c. If the resolvent is the empty clause, then a contradiction has been found. If it is
not, then add it to the set of c1auses available to the procedure.
 There are systematic strategies for making the choice of clauses to resolve together
each step so that we will find a contradiction if one exists. This can speed up the
process considerably.
o Only resolve pairs of clauses that contain complementary literals, since only
such resolutions produce new clauses that are harder to satisfy than their
parents. To facilitate this, index clauses by the predicates they contain,
combined with an indication of whether the predicate is negated Then, given a
particular clause, possible resolvent that contain a complementary occurrence
of one of its predicates can be located directly.
o Eliminate certain clauses as soon as they are generated so that they cannot
participate in later resolutions. Two kinds of clauses should be eliminated:
 Tautologies (which can never be unsatisfied) and
 Clauses that are subsumed by other clauses. For example, P⋁Q can be
subsumed by P.
o Whenever possible, resolve either with one of- the clauses that is part of the
statement we are trying to refute or with a clause generated by a resolution
with such a clause. This is called the “set-of-support strategy”.
o Whenever possible, resolve with clauses that have a single literal. Such
resolutions generate new clauses with fewer literals than the larger of their

Dr. Ram Prasad Reddy Sadi Page 18

 UNIT - II

parent clauses and thus are probably closer to the goal of a resolvent with zero
terms. This method is called the “unit-preference-strategy”.
Example 1:

Resolution Proof:

Dr. Ram Prasad Reddy Sadi Page 19