UNIT - II

Artificial Intelligence
III / II CSE, R 16 - JNTUK

Dr. T. K. Rao
VVIT

Dr. T. K. Rao - VVIT 1

Contents
• Problem reduction and game playing:
– Problem reduction 66
– Game playing 75
– Alphabeta pruning 93
– Two-player perfect information games 99
• Logic concepts:
– Propositional calculus
– Propositional logic
– Natural deduction system
– Axiomatic system
– Semantic tableau system in proportional logic
– Resolution refutation in proportional logic
– Predicate logic

Dr. T. K. Rao - VVIT 2

 Problem reduction
• Complex problems are divided into sub-problems using AND-OR graphs

• Solution of sub-problem may then be combined to obtain final solution

• E.g. Tower of Hanoi need problem reduction

• Objective of problem is to move entire stack of disks to another rod

• Only one disk may be moved at a time

• Each move consists of taking uppermost disk & sliding it onto another

• No disk will be placed on top of a smaller disk

Dr. T. K. Rao - VVIT 3

• Consider there are n disks on Rod1
• Move all n disks onto Rod2 making use of Rod3
• Lets develop an algorithm that can solve by reducing it to
smaller problems
• The game tree that is generated will contain AND-OR arcs
• Solution involves the following steps
• If n=1, move the only disk from Rod1 to Rod2
• If n>1, then move all the top n-1 disks in the same order
to other rod

Dr. T. K. Rao - VVIT 4

• Move the largest disk from Rod1 to Rod2
• Move finally all n-1 disks of Rod3 to Rod2
• So the problem is reduced to moving n-1 disks from
one rod to another
• First, from Rod1 to Rod3 and then from Rod3 to Rod2
• The same method can be employed both times by
renaming the rods
• The same strategy can be used to reduce the problem
of n-1 disks to n-2, n-3, etc. until only one disk is left
Dr. T. K. Rao - VVIT 5
Dr. T. K. Rao - VVIT 6
Dr. T. K. Rao - VVIT 7
• Consider an AND-OR Graph where each arc with a single successor
has a cost of 1
• Numbers given in () denote estimated cost of path
• Numbers given in [] represent revised cost of path
• Begin search from A & compute the heuristic values for its
successors, i.e. B & (C,D) as 19 & (8,9) respectively
• Estimated cost of paths from A to B is 20 & from A to (C,D) is 19,
which is a better path, So, expand this path, C to (G,H) & D to ( I,J)
• Heuristic values of G,H,I & J are 3,4,8,7 resp., which lead to revised
costs of C & D as 9 & 17 resp.
• The revised costs of path from A to (C,D) is calculated as 28, is not
the best path now
Dr. T. K. Rao - VVIT 8
Dr. T. K. Rao - VVIT 9
• So chose the path from A to B for expansion,
heuristic value of B is 17, best path

• Further explore the path from A to B

• the process continues until either a solution is

found or all paths lead to dead ends,
indicating that there is no solution

Dr. T. K. Rao - VVIT 10

 Node status labelling procedure
• A node in an AND-OR graph may be either a terminal node or a non-
terminal AND/OR node
• The labels used to represent are:
– Terminal node: cannot be expanded further, if this is the goal node, then
label as ‘solved’ else ‘unsolved’
– Non-terminal AND node: is labelled as unsolved as soon as one of its
successors is found to be unsolvable, labelled as ‘solved ’ if all of its
successors are solved
– Non-terminal OR node: labelled as ‘solved’ if one of its successors is
labelled ‘solved’; labelled as ‘unsolved’ if all of its successors are found to
be unsolvable
Dr. T. K. Rao - VVIT 11
ALGORITHM:
1. Let G be a graph with only starting node INIT.
2. Repeat the followings until INIT is labelled as SOLVED or h(INIT) > FUTILITY
a) Select an unexpanded node from the most promising path from INIT (call it NODE)
b) Generate successors of NODE. If there are none, set h(NODE) = FUTILITY (i.e.,
NODE is unsolvable); otherwise for each SUCCESSOR that is not an ancestor of
NODE do the following:
i. Add SUCCESSSOR to G.
ii. If SUCCESSOR is a terminal node, label it SOLVED & set h(SUCCESSOR) = 0.
iii. If SUCCESSPR is not a terminal node, compute its h
c) Propagate the newly discovered information up the graph by doing the
following: let S be set of SOLVED nodes or nodes whose h values have been
changed and need to have values propagated back to their parents. Initialize S to
Node. Until S is empty repeat the followings:
i. Remove a node from S and call it CURRENT.
ii. Compute the cost of each of the arcs emerging from CURRENT. Assign
minimum cost of its successors as its h.
iii. Mark the best path out of CURRENT by marking the arc that had the min
cost in step ii
iv. Mark CURRENT as SOLVED if all of the nodes connected to it through new
labeled arc have been labeled SOLVED
v. If CURRENT has been labeled SOLVED or its cost was just changed,
propagate its new cost back up through the graph. So add all of the ancestors
of CURRENT to S.

Dr. T. K. Rao - VVIT 12

Dr. T. K. Rao - VVIT 13
Dr. T. K. Rao - VVIT 14
Dr. T. K. Rao - VVIT 15
Dr. T. K. Rao - VVIT 16
Dr. T. K. Rao - VVIT 17
 Game playing
• A game is a sequence of choices where each
choice is made from a no.of discrete alternatives

• Every sequence ends in certain outcome & every

outcome has a value for the opening player

• Only two-player games are considered in which

both the players have exactly opposite goals

Dr. T. K. Rao - VVIT 18

• Games can be classified into two types
– Perfect information games: both the players have access
to the same information about the game in progress, e.g.
Tic-Tac-Toe, Chess, etc.

– Imperfect information games: players have no access to

full information about game, e.g. cards, dice, etc.

• Study is restricted to discrete & perfect info. games

• A game is discrete if it contains a finite no.of states

Dr. T. K. Rao - VVIT 19

• A typical characteristic of a game is to look
ahead at future positions to succeed

• Search procedures for two player games are:

– Game problem Vs state space problem

– Status labelling procedure in Game tree

– Nim game problem

Dr. T. K. Rao - VVIT 20

 Game problem Vs state space problem

• State space problems have start & intermediate states,

rules/operations and a goal state

• Game problems also have a start, legal moves and winning

positions

Dr. T. K. Rao - VVIT 21

• Game begins from a specified initial state and ends in win
(for one player)/ loss (other)/ draw
• A game tree is an explicit representation of all possible plays
of the game
• Root node is an initial position of game, its successors are the
positions resulting from the second player’s moves and so on
• Terminal nodes are represented by WIN/ LOSS/ DRAW
• Each path to a terminal node represents a different complete
play of the game

Dr. T. K. Rao - VVIT 22

• In game theory, maximum possible loss is minimized
and minimum gain is maximized
• In game, two nodes are there, MAX & MIN
• MAX node tries to maximize its own game and
minimizes (MIN) the opponent’s game
• For this, generate the complete game tree with all
possible moves and then decide which move is the
best for MAX
• As a part of game playing, game trees labelled as MAX
level and MIN level are generated alternately
Dr. T. K. Rao - VVIT 23
Dr. T. K. Rao - VVIT 24
 Status labelling procedure in Game tree

• Each level is labelled in the game tree according to the

player who makes the move at that point
• Status labelling process is as follows

Dr. T. K. Rao - VVIT 25

Dr. T. K. Rao - VVIT 26
Dr. T. K. Rao - VVIT 27
 Nim game problem
• The Game: There is a single pile of match sticks (>1) and two
players
• Moves are made by the players alternately
• Each player can pick up a max of half the no.of match sticks
in the pile
• Whoever takes the last match stick, loses
• We will develop complete game tree with either MAX or MIN
playing as first player

Dr. T. K. Rao - VVIT 28

Dr. T. K. Rao - VVIT 29
• Each node contains the total no.of sticks in the pile
and is labelled as W / L with procedure
• If a single stick is left at MAX level, it is assigned L,
if one stick is left at MIN level then W is assigned
• Label W/L is assigned from MAX’s point of view at
leaf nodes
• Arcs carry the no.of sticks to be removed
• Dotted lines show the propagation of status
• Thick lines show the winning path in following fig
Dr. T. K. Rao - VVIT 30
Dr. T. K. Rao - VVIT 31
• Strategy: if at the time of MAX’s turn there are N
sticks are in a pile, then MAX can force a win by
leaving M sticks for the MIN to play
• M ϵ {1,3,7,15,31,63,…} using the rule of game
• The sequence can be generated using the formula
Xi=2Xi-1+1, where X0=1 for i>0
• To formulate a method which determine the
number of sticks to be picked by MAX, there are
two ways

Dr. T. K. Rao - VVIT 32

• First is, from sequence figure out the closest
number less than the given number N sticks
• The difference b/w N and that number gives the
desired no.of sticks that have to be picked
• E.g. if N=45, closes no. is 31, then 45-31=14,
hence 14 sticks are to be picked by MAX
• Second is, the desired number is obtained by
removing the MSB from the binary
representation of N and adding it to the LSB

Dr. T. K. Rao - VVIT 33

Dr. T. K. Rao - VVIT 34
 Validity cases for winning of MAX player

• Case 1: If MAX is first player & N∉ {3,7,15,31,63,…}, then MAX

always win.

• Consider a pile of 29 sticks and let MAX be the first player.

• The complete game tree is shown in next slide.

• From the figure, it can be seen that MAX always wins.

• This case is validated for any no. of sticks ∉ { 3,7,15,31,63,…}

• From figure, MAX is bound to win irrespective of how MIN plays.

Dr. T. K. Rao - VVIT 35

Dr. T. K. Rao - VVIT 36
• Case 2: If MAX is the second player and N ∈
{3,7,15,31,63,…}, then MAX always win.

• Consider a pile of 15 sticks and let MAX be the

second player.

• Complete game tree is shown in fig.

• From figure, it can be seen that MAX always wins.

• This case is validated for any no. of sticks ∈ {

3,7,15,31,63,…}
Dr. T. K. Rao - VVIT 37
Dr. T. K. Rao - VVIT 38
• Case 3: If MAX is the first player and N ∈ {3,7,15,31,63,…} at the root of
the game, then MAX can force a win using the strategy mentioned in all
cases except when MAX gets a number from the sequence {3,7,15,31,63..}
at its turn.

• Assume that N=15, figure shows that MAX wins in all cases except when it
gets 7 matchsticks in its turn.

• MAX even can win the game when it gets 7 sticks at its turn in game for all
values except when it gets 3 sticks at its turn in the game.

• MAX is playing with M sticks ∈ {3,7,15, 31, 63,..} at any point in the game,
it can win for all cases except for the case when it gets value 3.

• MAX can win in these situations if opponent is playing without any

strategy.
Dr. T. K. Rao - VVIT 39
Dr. T. K. Rao - VVIT 40
• Case 4: If MAX is second player & N ∉ {3,7,15,31,63,..}
at the root of the game, then MAX can force a win
using the strategy mentioned in all cases except when
MAX gets a number from sequence {3,7,15,31,63,…} at
its turn.

• Assume that N=29, let MIN be the first player.

• The figure shown in next slide shows that MAX wins all
cases except when it gets 15 matchsticks at its turn.

• MAX might lose in case of it getting 15.

Dr. T. K. Rao - VVIT 41
Dr. T. K. Rao - VVIT 42
 Alphabeta pruning
• Also known as backward pruning
• Used to reduce no.of branches explored and no.of
static evaluations applied
• Requires two threshold values,
– one represents lower bound(α) on the value that a
maximizing node may be assigned
– another represents upper bound (β) on the value that a
minimizing node may be assigned

Dr. T. K. Rao - VVIT 43

• Each MAX node has an α value which never decreases
& each MIN node has a β value which never increases
• These values are set and updated when the value of a
successor node is obtained.
• The search is depth-first and stops at any MIN node
whose beta value is smaller than or equal to the alpha
values of its parent
• MAX node whose alpha value is greater than or equal
to the beta value of its parent

Dr. T. K. Rao - VVIT 44

MAX α = -∞; β = ∞

MIN

MAX

MIN

10 5 7 11 12 8 9 8 5 12 11 12 9 8 7 10
Dr. T. K. Rao - VVIT 45
• At maximizing level, β to determine whether search is cut-
off
• At the minimizing level, α to prune the search
• Values of α & β must be known at the levels to pass to the
next levels in the tree
• Each level should have both values; one to use & other to
pass to the next level
• The effectiveness of α-β pruning procedure depends greatly
on the order in which the paths are examined.
• If worst paths are examined first, there will be no cut-offs
Dr. T. K. Rao - VVIT 46
Two-player perfect information games
• Chess
• Checkers
• Othello
• Go
• Backgammon

Dr. T. K. Rao - VVIT 47

 Chess
• First two chess programs were proposed by Greenblatt, et
al. & Newell & Simon
• Played on a chequered board (64 squares in 8X8 square)
• Opponent’s king has to be placed such that where king is
under immediate attack & no way to save it from attack
(Checkmate)
• Players should avoid making moves that may place their
king under direct threat (or check)

Dr. T. K. Rao - VVIT 48

Dr. T. K. Rao - VVIT 49
 Checkers
• First developed by Arthur Samuel and it had a learning
component to improve player performance

• In a 8X8 square board, each player gets 12 pieces of the

same color which are placed on the dark squares of the
board in three rows

• The row closest to a player is called the king row

• Pieces in king row are kings and other pieces are men

Dr. T. K. Rao - VVIT 50

• King can move diagonally forward & backward, men
can move diagonally forward only

• Opponent’s pieces can be removed by diagonally

jumping over them

• When men pieces jump over king pieces of the

opponent, they transform into kings

• Objective of game is to remove all pieces of opponent

from board or by leading opponent to such a situation
where player left with no legal moves
Dr. T. K. Rao - VVIT 51
Dr. T. K. Rao - VVIT 52
 Othello
• Also called Reversi, played on 8X8 square grid with pieces that have two
distinct bi-colored sides
• The pieces are shaped as coins and possesses a light and dark face, each
face representing one player
• The objective of game is to make your pieces constitute a majority of the
pieces on board at the end of game, by turning over as many of your
opponent’s pieces as possible
• Advanced computer programs for Othello were developed by Rosenbloom
in 1982 and subsequently Lee & Mahajan in 1990
https://www.youtube.com/watch?v=s-_Slk35qSw

Dr. T. K. Rao - VVIT 53

Dr. T. K. Rao - VVIT 54
 Go
• In this, players play alternatively by placing black &
white stones on vacant intersections of 19X19 board
• Objective of game is to control larger portion of board
than opponent
• To achieve this, players try to place their stones in such
a way that they cannot be captured by opponent
• Placing stones close to each other helps them support
one another and avoid capture
Dr. T. K. Rao - VVIT 55
• Placing them far apart creates an influence across
a larger part of the board
• A stone or a group of stones is captured and
removed if it has no empty adjacent intersections
• i.e., it is completely surrounded by stones of
opponent player
• When neither side can increase its territory or
reduce that of its opponent’s, score is counted
and game is declared over
Dr. T. K. Rao - VVIT 56
Dr. T. K. Rao - VVIT 57
Dr. T. K. Rao - VVIT 58
 Backgammon
• It is a two-player game where each player has 15 pieces
(checkers or men) that move between 24 triangles (points)
according to the roll of two dice

• Objective is to be first to bear off, i.e. move all fifteen checkers

off the board

• Backgammon involves a combination of strategy and luck

(from rolling dice). While the dice may determine the outcome
of a single game, the better player will accumulate the better
record over a series of many games.
Dr. T. K. Rao - VVIT 59
• Objective of game is to remove all checkers from board
before opponent can do the same
• With each role of dice a player must choose from
numerous options for moving his checkers and anticipate
possible counter moves by the opponent
• Players may raise stakes during the game
• Backgammon programs with high level of competence
were developed by Berlier in 1980 and by Tesauro &
Sejnowski in 1989.
• https://www.youtube.com/watch?v=xXE5AwzNQ2s

Dr. T. K. Rao - VVIT 60

Dr. T. K. Rao - VVIT 61
 Propositional Calculus
• A set of rules are used to combine simple propositions
to form compound propositions, using logical operators
• These logical operators are known as connectives
• E.g. not(~), and(۸), or(۷), implies(->), equivalence (<->),
etc.
• A well formed formula is defined as a symbol or a string
of symbols, generated by formal grammar of a formal
language
Dr. T. K. Rao - VVIT 62
• The smallest unit or an atom is considered to be a
well-formed formula
• If α is a well-formed formula, then ~α is also a well
formed formula
• If α and β are well-formed formula, then (α ۸β),
(α۷β ), (α -> β ), (α <-> β ) are also well-formed
formulae
• A propositional expression is called a well-formed
formula if and only if it satisfies the above
properties Dr. T. K. Rao - VVIT 63
 Truth table
• A Truth Table is used to provide operational definitions of important
logical operators
• It elaborates all possible truth values of a formulae
• The logical constants in PC are true and false, these are represented
as T and F in a truth table
• Let A, B, C… are assumed to be propositioned symbols
• The truth values of well formed formulae are calculated by using
the truth table approach

Dr. T. K. Rao - VVIT 64

Dr. T. K. Rao - VVIT 65
 Equivalence laws
• Definition: Two formulae α and β are said to be logically
equivalent (α ~ β) iff the truth values of both are same for
all possible assignments of logical constraints (T & F) to the
symbols appearing in the formulae

• Equivalence relations/ laws are used to reduce or simplify a

given well-formed formula or to derive a new formula from
the existing formula

• These laws can be verified using the truth table approach

Dr. T. K. Rao - VVIT 66
Dr. T. K. Rao - VVIT 67
Dr. T. K. Rao - VVIT 68
• Let us verify the absorption law A V (A^B) ~ A using
truth table approach as in table

A B A^B A V (A^B)
T T T T
T F F T
F T F F
F F F F

• we can clearly see that the truth values of A V (A^B)

and A are same; therefore these expressions are
equivalent

Dr. T. K. Rao - VVIT 69

 Propositional logic
• It deals with the validity, satisfiability (consistency), and
unsatisfiability (inconsistency) of a formula and the derivation of a
new formula using equivalence laws
• Each row of a truth table for a given formula “α” is called its
interpretation under which the valued of a formula may be either
true or false
• A formula α is said to be tautology iff the value of α is true for all its
interpretations
• The validity, satisfiability, and unsatisfiability of a formula may be
determined as follows:
Dr. T. K. Rao - VVIT 70
• A formula α is said to be valid iff it is tautology
• A formula α is said to be satisfiable if there exists at
least one interpretation for which α is true
• A formula α is said to be unsatisfiable if the value of α
is false under all interpretations
• E.g. if it is humid then it will rain and since it is humid
today it will rain
• Solution:
– A: It is humid
– B: It will rain
Dr. T. K. Rao - VVIT 71
• The formula α corresponding to the given
sentence is α: [(A->B)۸A]->B

Dr. T. K. Rao - VVIT 72

• Truth table approach is easy for evaluating consistency,
validity, etc. of a formula
• But the size of truth table grows exponentially
• If a formula contains n atoms, then the truth table will
contain 2n entries
• Some other methods are concerned are:
– Natural deduction system
– Axiomatic system
– Semantic tableu method
– Resolution refutation method

Dr. T. K. Rao - VVIT 73

 Natural deduction system
• NDS is thus called because it mimics the pattern
of natural reasoning
• The system is based on a set of deductive
inference rules
• Assuming that A1, A2,…Ak, where 1<=k<=n, are set
of atoms and αj, where 1<=j<=m, and β are well
formed formula
• The inference rules may be stated as in table
Dr. T. K. Rao - VVIT 74
Dr. T. K. Rao - VVIT 75
Dr. T. K. Rao - VVIT 76
• A theorem in NDS written as, from α1,… α2 infer β
leads to the interpretation that β is deduced from a set
of hypotheses {α1,… α2} are assumed to be true in a
given context
• Therefore the theorem β is also true in same context
• Thus we can conclude that β is consistent
• A theorem that is written as infer β implies that there
are no hypotheses and β is true under all
interpretations, i.e. β is a tautology

Dr. T. K. Rao - VVIT 77

• E.g. prove that A ۸ (B۷C) is deduced from A۸B

• Solution: The theorem in NDS can be written

as from A۸B infer A۸(B۷C) in NDS

Dr. T. K. Rao - VVIT 78

• If we assume A->B is true, then we can conclude
that B is also true if A is true

• It can be represented in the form of a theorem of

NDS as from A infer B and if we can prove the
theorem, then we can conclude the truth of A->B

• The converse of this is also true

• Let us state formally the deduction theorem in

NDS
Dr. T. K. Rao - VVIT 79
• Deduction theorem: to prove a formula
A1^A2^…An -> B, it is sufficient to prove a
theorem from A1, A2, .. An infer B
• Conversely if A1^A2^…An -> B is proved then
the theorem from A1, A2, .. An infer B
assumed to be proved
• Let us consider the example to show the use
of deduction theorem
Dr. T. K. Rao - VVIT 80
Dr. T. K. Rao - VVIT 81
 Axiomatic system
• It is based on a set of three axioms and one rule of deduction
• A forward chaining approach
• It is as powerful as Truth table & NDS approach
• In this, a guess is required in selection of appropriate
axiom(s)
• In this, only two logical operators, not(~) and implication(->)
are allowed to forma a formula
• Any formula can be written using the ~ and ->
Dr. T. K. Rao - VVIT 82
• E.g.
– A۸B≡ ~(~A۷~B) ≡ ~(A->~B)
– A۷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 is called Modus
Ponen (MP) as follows:
– Axiom1: A->(B->A)
– Axiom2: [A->(B->C)]-> [(A->B)->(A->C)]
– Axiom3: (~A->~B)->(B->A)
– Rule: Hypothesis: A->B and A; consequent: B
Dr. T. K. Rao - VVIT 83
• Interpretation of Modus Ponen’s rule:
– Given that A->B and A are hypotheses (assumed to be true), B is
inferred (i.e., true) as a consequent

• E.g. Establish A->C is a deductive sequence of {A->B, B->C}, i.e.

{A->B,B->C} |- (A->C)

Dr. T. K. Rao - VVIT 84

 Semantic tableau system
• A backward chaining approach
• A set of rules are applied systematically on a
formula/ a set of formulae in order to establish
consistency or inconsistency
• Semantic Tableau is a binary tree constructed by
using semantic tableau rules with a formula as a
root
Dr. T. K. Rao - VVIT 85
Semantic Tableau rules

Dr. T. K. Rao - VVIT 86

Dr. T. K. Rao - VVIT 87
Dr. T. K. Rao - VVIT 88
E.g. construct a semantic tableau for a formula (A۸~B)۸ (~B->C)

Dr. T. K. Rao - VVIT 89

 Satisfiability and Unsatisfiability
• A path is said to be contradictory/ closed/ finished whenever
complementary atoms appear on the same path of a semantic
tableau

• If all paths of a tableau for a given formula α are found to be closed,

it is called a contradictory tableau

• This indicates that there is no interpretation/ model that satisfies α

• A formula α is said to be satisfiable if a tableau with root α is not a

contradictory tableau, i.e. it has at least one open path

Dr. T. K. Rao - VVIT 90

• A model or an interpretation can obtained under which the
formula α evaluated to be true by assigning T (true) to all
atomic formulae appearing on the open path or semantic
tableau of α
• A formula α is said to be unsatisfiable if a tableau with root
α is a contradictory tableau
• If we obtain a contradictory tableau with root ~α, we say
that the formula α is tableau provable
• Alternatively, a formula α is said to be tableau provable
(denoted by |- α) if a tableau with root ~α is a contradictory
tableau
Dr. T. K. Rao - VVIT 91
• S = {α1, α2, α3,.. αn} is said to be unsatisfiable if a tableau with
root (α1^α2^.. ^αn) is a contradictory tableau
• S = {α1, α2, α3,.. αn} is said to be satisfiable if the formulae in a
set are simultaneously true, i.e., if a tableau for (α1^α2^.. ^αn)
has at least one open/ non-contradictory path
• Let S be a set of formulae, the formula α is said to be tableau
provable from S (denoted by S |- α) if there is a contradictory
tableau from S with ~α as a root
• A formula α is said to be a logical consequence of a set S iff α is
tableau provable from S
• If α is tableau provable (|- α) then it is also valid (|= α) & vice
versa
Dr. T. K. Rao - VVIT 92
Dr. T. K. Rao - VVIT 93
Dr. T. K. Rao - VVIT 94
Dr. T. K. Rao - VVIT 95
Dr. T. K. Rao - VVIT 96
 Resolution refutation
• This method is used to derive a goal from a given set of clauses by
contradiction
• Clause denotes a special formula containing the Boolean operators
~ and ۷
• Any formula can be converted into a set of clauses
• Resolution refutation is used to develop computer-based-systems
that can be used to prove theorems automatically
• This uses a single inference rule, ‘resolution based on modus ponen
inference rule’

Dr. T. K. Rao - VVIT 97

• This method is more efficient than NDS and Axiomatic
system because, in this, we do not need to guess which
rule or axiom to apply in development of proofs
• Here, 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
• During resolution, two clauses are needed to be
identified for the application of resolution rule:
– One is with a positive atom (P)
– Second is with a negative atom (~P)
Dr. T. K. Rao - VVIT 98
Dr. T. K. Rao - VVIT 99
• Conversion of formula into a set of clauses:
– There are two normal forms in Propositional Logic, viz.,
Disjunctive Normal Form (DNF) & Conjunctive Normal Form
(CNF)
– A formula is said to be in its normal form if it is constructed
using only natural connectives {~, ۸, ۷}
– Formula is represented as disjunction of conjunction, i.e.,
(L11 ۸ L12 ۸ .. ۸ L1m) ۷ .. ۷ (Lp1 ۸ Lp2 ۸ .. ۸ Lpm) in DNF
– Formula is represented as conjunction of, disjunction i.e.,
(L11 ۷ L12 ۷ .. ۷ L1m) ۸ .. ۸ (Lp1 ۷ Lp2 ۷ .. ۷ Lpm) in CNF
– Here are Lij are literals (positive or negative atoms)
Dr. T. K. Rao - VVIT 100
• CNF can easily be written for a given formula, (C1 ۸ .. ۸ Cn),
where each Ck (1 <= K <= n) is a disjunction of literals and is
called a clause
• A clause is defined as a formula of the form (L1 ۷ L2 ۷.. ۷ Lm)
• Therefore, if a given formula is converted to its equivalent
CNF as (C1 ۸ .. ۸ Cn), then the set of clauses is nothing but a
set of each conjunct of CNF, i.e., {C1, C2, .. Cn}
• E.g. the set {A ۷ B, ~A V D, C ۷ ~B} represents a set of
clauses A V B, ~A ۷ D, & C ۷ ~B

Dr. T. K. Rao - VVIT 101

Conversion of a Formula to its CNF
Any formula in Propositional logic can be transformed into its
equivalent CNF representation by using equivalence laws as follows:
• Eliminate double negation signs by using
– ~(~A) ≡ A
• Use DE-Morgan's Laws to push ~ immediately before the atomic
formula
– ~(A ᴧ B) ≡ ~A v ~B
– ~(A v B) ≡ ~A ᴧ ~B
• Use distributive law to get CNF
– A v (B ᴧ C) ≡ (A v B) ᴧ (A v C)

Dr. T. K. Rao - VVIT 102

• Eliminate → and ↔ by using the following
equivalence laws
• A → B ≡ ~A v B

• A ↔ B ≡ (A → B ) ᴧ (B → A)

E.G. Convert (~A → B) ᴧ ( C ᴧ ~A) into CNF

• (~(~A) v B) ᴧ ( C ᴧ ~A)

• (A V B) ᴧ C ᴧ ~A

Set of clauses in this case is written as {(A V B), C , ~A}

Dr. T. K. Rao - VVIT 103

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 remaining literals in both clauses
• If two clauses C1 and C2 contain a complementary pair of
literals {L,~L}, then new clause C may be constructed by
eliminating L.
• Here, C1 and C2 are called parent clauses and C is called
resolvent
• The resolution tree is invert of Binary tree with last node
being a resolvent Dr. T. K. Rao - VVIT 104
Find the resolvent of {A v B, ~A v D, C v ~B }

Dr. T. K. Rao - VVIT 105

 Resolution Process
• If C is resolvent of two clauses C1 and C2, then C is
called a logical sequence of the clauses {c1,c2}
• This is known as resolution principle.
• If a contradiction is derived from a set 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.
Dr. T. K. Rao - VVIT 106
• Using resolution refutation principle show that C v D
is a logical sequence of { A v B, ~A v D, C v ~B}

Dr. T. K. Rao - VVIT 107

Dr. T. K. Rao - VVIT 108
 Predicate logic
• Propositional logic has many limitations
• E.g. John is a boy, Paul is a boy, Peter is a boy
– It can be symbolized by A,B, & C respectively in propositional logic
– But no conclusions can be drawn similarities among boys, i.e. A, B,
C cannot represent boys
• So, a general statement boy(X), where X is bound with John,
Paul, Peter
• These facts are called instances of a boy(X)
• Here, boy(X) is called a Predicate statement or expression,
boy is predicate symbol, X is argument
Dr. T. K. Rao - VVIT 109
• When a variable X gets bound to its actual value then
predicate statement boy(X) becomes either true / false

• E.g. boy(Peter) = true, boy(Marry) = false

• Predicate logic is a logical extension of Propositional logic

• Statements like “All birds fly” cannot be represented in

Propositional logic

• Such limitations are removed in Predicate logic

• Predicate calculus is the study of predicate systems

• When inference rules are added to predicate calculus, it

becomes predicate logic
Dr. T. K. Rao - VVIT 110
 Predicate Calculus
• It has three more logical notions in addition to Propositional
calculus

• Term: A term is either a variable, or constant or n-place

function. f(t1, t2,…, tn)

• Predicate: A predicate is defined as a relation that maps n

terms to a truth value {true, false}

• Quantifiers: Quantifiers are used with variables. There are

two types of quantifiers, namely Universal quantifiers, ∀,(For
all), and, existential quantifiers, ∃ (there exists)
Dr. T. K. Rao - VVIT 111
• Variables are denoted by upper case letters (X, Y, Z ...)

• Predicate symbols are denoted by lower case letters (p, q, r..)

• Constants are represented as 6, john, tree..

• Functions are represented by lower case letters (f, g, h ..)

Well formed formula(WFF):

• Atomic formula p(t1, t2,…,tn) is a WFF, p is predicate symbol &

t1, t2,… tn are terms

• If α & β are WFF, ~α, α ˄ β , α v β, α → β , α ↔ β are WFF

• If α is a WFF & X is free variable in α, then (∀ X) α & (∃X) α are

also WFF
Dr. T. K. Rao - VVIT 112
 Predicate Calculus Types
• First Order Predicate Calculus: If the quantification in
predicate formula is only on simple variables and not
on predicates or functions.

Eg. ∀ X ∀ Y(p(X) ↔ p(Y))

• Second Order Predicate Calculus: If this quantification

is over first order predicates and functions.

Eg. ∀ p (p(X)) ↔ p(Y)

Dr. T. K. Rao - VVIT 113
Interpretations of Formulae in FOL
• Each formula α is evaluated to be true or false under a given
interpretation I over a given domain D:
• (∀ X) p(X) = true iff p(X)= true, ∀ X ϵ D otherwise it is false.
• (∃ X) p(X) = true if and only if ∃ c ϵ D such that p(c) = true,
otherwise it is false.
E.g: Evaluate the truth value of an FOL formula α: (∀X) (∃Y) p(X,
Y) under the following interpretation I: D={1, 2}; p(1, 1) = F
Sol: for X=1 then ∃ 2 ϵ D such that p(1, 2)=T, p(2, 1)=T, p(2, 2)=F.
Hence, α is true under interpretation I
Dr. T. K. Rao - VVIT 114
• Evaluate α: (∀ X)[p(X)q(f(X),c)] under the following interpretation:
– D = {1, 2}

– c = 1 {c is a constant from the domain D}

– f(1) = 2, f(2) = 1

– p(1) = F, p(2) = T

– q(1, 1) = T, q(1, 2)=T, q(2, 1) = F, q(2, 2) = T

• For X=1

p(1)  q(f(1), 1) = p(1)  q(2, 1) = F  q(2, 1) = F  F = T

• For X=2

p(2)  q(f(2), 1) = p(2)  q(1, 1) = T  q(1, 1) = T  T = T

α is true for all values of XЄ D under the interpretation I

Dr. T. K. Rao - VVIT 115
Satisfiability and Unsatisfiability in FOL
• A formula α is said to be satisfiable iff ∃ an interpretation I such
that α is evaluated to be true under I
• Alternatively, we may say that I is a model of α or I satisfies α.
• A formula α is said to be unsatisfiable iff ∃ no interpretation that
satisfies α or ∃ no model for α
• A formula α is said to be valid iff ∀ interpretation I, α is true.
• A formula α is called a logical consequence of a set of formulae
{α1, α2,…, αn} iff ∀ interpretation I, if (α1 ᴧ α2 ᴧ … ᴧ αn) is
evaluated to be true, then α is also evaluated to be true.

Dr. T. K. Rao - VVIT 116

 Transformation of a Formula into
Prenex Normal Form

• A formula is said to be in closed form if all the variables

appearing in it are quantified & no free variables there are

• Prenex Normal Form: A closed formula α in FOL is said to

be in PNF iff α is represented as (Q1, X1) (Q2, X2) … (Qn, Xn)
M, where Qk are qualifiers (∀ or ∃), Xk are variables, for
(1 <= k <= n), while M is a formula free from quantifiers.

Dr. T. K. Rao - VVIT 117

 Conversion of a Formula into Prenex
Normal Form
• A formula can be transformed or converted into
PNF using various equivalence laws.
• Conventions:
• α - FOL formula α without a variable X
• α [X] – FOL formula α which contains a variable X
• Q – Quantifier (∀ or ∃)
Dr. T. K. Rao - VVIT 118
 Equivalence Laws
• Law 1: (QX) α [X] *β ≡ (QX) (α [X] * β)

• Law 2: α * Q(X) β[X] ≡ (QX) (α * β [X])

• Law 3: ~(∀ X) α [X] ≡ (∃X)(~ α [X])

• Law 4: ~(∃X) α [X] ≡ (∀ X) (~α [X])

• Law 5: (∀ X) α [X] ˄ (∀ X) β[X] ≡ (∀ X) (α [X] ˄ β[X] )

• Law 6: (∃ X) α [X] ˅ (∃ X) β[X] ≡ (∃ X) (α [X] ˅ β[X] )

Dr. T. K. Rao - VVIT 119

 Conversion of PNF to Standard form
(Skolemization)
• The process of eliminating existential
quantifiers from the prefix of PNF notation
replacing the corresponding variable by a
constant or a function is called skolemization,
such a constant, or a function is called skolem
constant or skolem function, respectively.

Dr. T. K. Rao - VVIT 120

 Skolemization Procedure
• Scan prefix from left to right till we obtain the
first existential quantifier
– If Q1 is the first existential quantifier then choose
a new constant c ∉ {set of constants in M}.
Replace all occurrences of X1 appearing in matrix
M by c and delete (Q1 X1) from the prefix to
obtain the new prefix and matrix
Dr. T. K. Rao - VVIT 121
 – If Qr is the first existential quantifier and Q1 Q2… Qr-1
are universal quantifiers appearing before Qr, then
choose a new (r-1) place function symbol f ∉ {set of
functions appearing in M}. Replace all occurrence of
Xr in M by f(X1, X2,…Xr-1) and remove (Qr Xr) from
prefix

• Repeat the process till all existential quantifiers

are removed from M

Dr. T. K. Rao - VVIT 122

Eg.1: Every philosopher writes at least one
book. ∀x[Philo(x) → ∃y[Book(y) ∧ Write(x, y)]]
Eliminate Implication:
∀x[¬Philo(x) ∨ ∃y[Book(y) ∧ Write(x, y)]]
Skolemize: substitute y by g(x)
∀x[¬Philo(x) ∨ [Book(g(x)) ∧ Write(x, g(x))]]

Dr. T. K. Rao - VVIT 123

Eg. 2: All students of a philosopher read one of
their teacher’s books.

∀x∀y[Philo(x) ∧ StudentOf (y, x) → ∃z[Book(z) ∧

Write(x, z) ∧ Read(y, z)]]

All students of a philosopher read one of their

teacher’s books.

∀x∀y[Philo(x) ∧ StudentOf (y, x) → ∃z[Book(z) ∧

Write(x, z) ∧ Read(y, z)]]
Dr. T. K. Rao - VVIT 124
Eliminate Implication:

∀x∀y[¬Philo(x) ∨ ¬StudentOf (y, x) ∨ ∃z[Book(z)

∧ Write(x, z) ∧ Read(y, z)]]

Skolemize: substitute z by h(x, y)

∀x∀y[¬Philo(x) ∨ ¬StudentOf (y, x) ∨ [Book(h(x,

y)) ∧ Write(x, h(x, y)) ∧ Read(y, h(x, y))]]

Dr. T. K. Rao - VVIT 125

• There exists a philosopher with students.
∃x∃y[Philo(x) ∧ StudentOf (y, x)

• There exists a philosopher with students.

∃x∃y[Philo(x) ∧ StudentOf (y, x)]

• Skolemize: substitute x by a and y by b

• Philo(a) ∧ StudentOf (b, a)

Dr. T. K. Rao - VVIT 126