Artificial Intelligence
Module 5
Artificial Intelligence Module 5
BCS545B
Syllabus
• Inference in First Order Logic
• Classical Planning
– Artificial Intelligence: Start Russell, Peter Norvig
Chapter 9 (9.4, 9.5) and
Chapter 10 (10.1, 10.2, 10.3)
Artificial Intelligence Module 5
BCS545B
Inference in First Order
Logic
Chapter 1
Artificial Intelligence Module 5
BCS545B
Topics Covered in this Chapter
• Backward Chaining
• Resolution
Artificial Intelligence Module 5
BCS545B
Backward Chaining
• What is Backward Chaining?
– Backward Chaining is a goal-driven reasoning approach used in logic programming
and expert systems.
– The process starts with a goal or hypothesis and works backward to determine if
there is evidence or facts that support it.
– It is used in deductive systems like Prolog, where the goal is to confirm the validity of
a hypothesis based on known facts.
Artificial Intelligence Module 5
BCS545B
Backward Chaining Problem
• The law says that it is crime for an American to sell weapons to hostile nations.
The country Nono, an enemy of America, has some missiles, and all of its
missiles were sold to it by Colonel West, who is an American. An enemy of
America counts as “hostile”
Prove “West is Criminal”
∀x∀y∀z: American(x) ^ Weapon(y) ^ Sells(x, y, z) ^ Hostile(z) => Criminal(x)
∀x: Missile(x) ^ Owns(Nono, x) => Sells(West, x, Nono)
•
∀x: Enemy(x, America) => Hostile(x)
•
∀x: Missile(x) => Weapon(x)
•
•
• American(West)
• Enemy(Nono, America)
• Owns(Nono, M1)
• Missile(M1)
Artificial Intelligence Module 5
BCS545B
Logic Programming
• Logic Programming is a programming language paradigm in which
logical assertions are viewed as programs.
• Example:
∀x: pet(x) small(x) apartmentPet(x)
∀x: cat(x) dog(x) pet(x)
–
∀x: poodle(x) dog(x) small(x)
–
poodle(fluffy)
–
–
apartmentPet(x) :- pet(x), small(x)
pet(x) :- cat(x)
–
pet(x) :- dog(x)
–
Prolog
dog(x) :- poodle(x)
–
small(x) :- poodle(x)
–
Programming
poodle(fluffy)
–
–
Artificial Intelligence Module 5
BCS545B
Resolution
• 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 to be true.
• Use 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
Artificial Intelligence Module 5
BCS545B
Resolution Convert to clause form
• Algorithm:
– Eliminate , using the fact that ab is equivalent to aVb.
– Reduce the scope of each to asingle term, using:
• (p) = p
• deMorgan’s laws:
– (ab) = aVb
– (aVb) = ab
• ∀xP(x) = P(x)
• xP(x) = P(x)
– Standardize variables
• ∀x:P(x) V ∀x:Q(x) can be written as ∀x:P(x)V ∀y:P(y)
Move all quantifiers to the left of the formula without changing their relative order
Eliminate Existential quantifiers using a skolem function
–
Drop the prefix
–
Convert the expression into a conjuction of disjuncts [(a = (aVc) (bVc)]
–
Create a separate clause for each conjunct
–
–
– Standardize apart the variables in the set of clauses generated in previous step ∀x:P(x) Q(x) =
∀x:P(x) ∀x:Q(x)
Artificial Intelligence Module 5
BCS545B
Resolution Problem
• The law says that it is crime for an American to sell weapons to hostile nations.
The country Nono, an enemy of America, has some missiles, and all of its
missiles were sold to it by Colonel West, who is an American. An enemy of
America counts as “hostile”
Prove “West is Criminal”
∀x∀y∀z: American(x) ^ Weapon(y) ^ Sells(x, y, z) ^ Hostile(z) => Criminal(x)
∀x: Missile(x) ^ Owns(Nono, x) => Sells(West, x, Nono)
•
∀x: Enemy(x, America) => Hostile(x)
•
∀x: Missile(x) => Weapon(x)
•
•
• American(West)
• Enemy(Nono, America)
• Owns(Nono, M1)
• Missile(M1)
Artificial Intelligence Module 5
BCS545B