Artificial Intelligence Tutorial

Introduction to Artificial Intelligence Intelligent Agents

Search Algorithms

Problem-solving Uninformed Search Informed Search Heuristic Functions Local Search Algorithms and Optimization Problems Hill Climbing search Differences in Artificial Intelligence Adversarial Search in Artificial Intelligence Minimax Strategy Alpha-beta Pruning Constraint Satisfaction Problems in Artificial Intelligence Cryptarithmetic Problem in Artificial Intelligence

Knowledge, Reasoning and Planning

Knowledge based agents in AI Knowledge Representation in AI The Wumpus world Propositional Logic Inference Rules in Propositional Logic Theory of First Order Logic Inference in First Order Logic Resolution method in AI Forward Chaining Backward Chaining Classical Planning

Uncertain Knowledge and Reasoning

Quantifying Uncertainty Probabilistic Reasoning Hidden Markov Models Dynamic Bayesian Networks Utility Functions in Artificial Intelligence


What is Artificial Super Intelligence (ASI) Artificial Satellites Top 7 Artificial Intelligence and Machine Learning trends for 2022 8 best topics for research and thesis in artificial intelligence 5 algorithms that demonstrate artificial intelligence bias AI and ML Trends in the World AI vs IoT Difference between AI and Neural Network Difference between Artificial Intelligence and Human Intelligence Virtual Assistant (AI Assistant) ARTIFICIAL INTELLIGENCE PAINTING ARTIFICIAL INTELLIGENCE PNG IMAGES Best Books to learn Artificial Intelligence Certainty Factor in AI Certainty Factor in Artificial Intelligence Disadvantages of Artificial Intelligence In Education Eight topics for research and thesis in AI Engineering Applications of Artificial Intelligence Five algorithms that demonstrate artificial intelligence bias 6th Global summit on artificial intelligence and neural networks Acting Humanly In Artificial Intelligence AI and ML Trends in the World AI vs IoT Artificial Communication Artificial intelligence assistant operating system Artificial Intelligence in Pharmacy Artificial Intelligence in Power Station Artificial Intelligence in Social Media Artificial Intelligence in Supply Chain Management Artificial Intelligence in Transportation Artificial Intelligence Interview Questions and Answers Artificial Intelligence Jobs in India For Freshers Integration of Blockchain and Artificial Intelligence Interesting Facts about Artificial Intelligence Machine Learning and Artificial Intelligence Helps Businesses Operating System Based On Artificial Intelligence SIRI ARTIFICIAL INTELLIGENCE SKILLS REQUIRED FOR ARTIFICIAL INTELLIGENCE Temporal Models in Artificial Intelligence Top 7 Artificial Intelligence and Machine Learning trends for 2022 Types Of Agents in Artificial Intelligence Vacuum Cleaner Problem in AI Water Jug Problem in Artificial Intelligence What is Artificial Super Intelligence (ASI) What is Logic in AI Which language is used for Artificial Intelligence Essay on Artificial Intelligence Upsc Flowchart for Genetic Algorithm in AI Hill Climbing In Artificial Intelligence IEEE Papers on Artificial Intelligence Impact of Artificial Intelligence On Everyday Life Impact of Artificial Intelligence on Jobs The benefits and challenges of AI network monitoring

Resolution Method in AI

Resolution Method in AI

Resolution method is an inference rule which is used in both Propositional as well as First-order Predicate Logic in different ways. This method is basically used for proving the satisfiability of a sentence. In resolution method, we use Proof by Refutation technique to prove the given statement.

The key idea for the resolution method is to use the knowledge base and negated goal to obtain null clause (which indicates contradiction). Resolution method is also called Proof by Refutation. Since the knowledge base itself is consistent, the contradiction must be introduced by a negated goal. As a result, we have to conclude that the original goal is true.

Resolution Method in Propositional Logic

In propositional logic, resolution method is the only inference rule which gives a new clause when two or more clauses are coupled together.

Using propositional resolution, it becomes easy to make a theorem prover sound and complete for all.

The process followed to convert the propositional logic into resolution method contains the below steps:

  • Convert the given axiom into clausal form, i.e., disjunction form.
  • Apply and proof the given goal using negation rule.
  • Use those literals which are needed to prove.
  • Solve the clauses together and achieve the goal.

But, before solving problems using Resolution method, let’s understand two normal forms

Conjunctive Normal Form (CNF)

In propositional logic, the resolution method is applied only to those clauses which are disjunction of literals. There are following steps used to convert into CNF:

1) Eliminate bi-conditional implication by replacing A ? B with (A ? B) ? (B ?A)

2) Eliminate implication by replacing A  ?   B with ¬A V B.

3) In CNF, negation(¬) appears only in literals, therefore we move it inwards as:

  • ¬ ( ¬A) ? A (double-negation elimination
  • ¬ (A ? B) ? ( ¬A V ¬B) (De Morgan)
  • ¬(A V B) ? ( ¬A ? ¬B) (De Morgan)

4) Finally, using distributive law on the sentences, and form the CNF as:

(A1 V B1) ? (A2 V B2) ? ….  ? (An V Bn).

Note: CNF can also be described as AND of ORS

Disjunctive Normal Form (DNF)

This is a reverse approach of CNF. The process is similar to CNF with the following difference:

(A1 ? B1) V (A2 ? B2) V…V (An ? Bn). In DNF, it is OR of ANDS, a sum of products, or a cluster concept, whereas, in CNF, it is ANDs  of Ors.

Example OF Propositional Resolution

Consider the following Knowledge Base:

  1. The humidity is high or the sky is cloudy.
  2. If the sky is cloudy, then it will rain.
  3. If the humidity is high, then it is hot.
  4. It is not hot.

Goal: It will rain.

Use propositional logic and apply resolution method to prove that the goal is derivable from the given knowledge base.

Solution: Let’s construct propositions of the given sentences one by one:

  1. Let, P: Humidity is high.

                    Q: Sky is cloudy.

It will be represented as P V Q.

2) Q: Sky is cloudy.                      …from(1)

Let, R: It will rain.

It will be represented as b?  R.

3) P: Humidity is high.                 …from(1)

Let, S: It is hot.

It will be represented as P  ?   S.

4) ¬S: It is not hot.

Applying resolution method:

In (2), Q ? R will be converted as (¬Q V R)

In (3), P ?  S will be converted as (¬P V S)

Negation of Goal (¬R): It will not rain.

Finally, apply the rule as shown below:

Negation of Goal (¬R):

After applying Proof by Refutation (Contradiction) on the goal, the problem is solved, and it has terminated with a Null clause ( Ø ). Hence, the goal is achieved. Thus, It is not raining.

Note: We can have many examples of Proposition logic which can be proved with the help of Propositional resolution method.

Resolution Method in FOPl/ Predicate Logic

Resolution method in FOPL is an uplifted version of propositional resolution method.

In FOPL, the process to apply the resolution method is as follows:

  • Convert the given axiom into CNF, i.e., a conjunction of clauses. Each clause should be dis-junction of literals.
  • Apply negation on the goal given.
  • Use literals which are required and prove it.
  • Unlike propositional logic, FOPL literals are complementary if one unifies with the negation of other literal.

For example: {Bird(F(x)) V Loves(G(x), x)} and {¬Loves(a, b) V ¬Kills(a, b)}

Eliminate the complementary literals Loves(G(x),x) and  Loves(a,b)) with ? ={a/G(x), v/x} to give the following output clause:

{Bird(F(x)) V ¬Kills(G(x),x)}

The rule applied on the following example is called Binary Resolution as it has solved exactly two literals. But, binary resolution is not complete. An alternative approach is to extend the factoring i.e., to remove redundant literals to the first order case. Thus, the combination of binary resolution and factoring is complete.

Conjunctive Normal Form

There are following steps used to convert into CNF:

  • Eliminate the implications as:

?x: A(x)   ?     B(x) with {¬ x: ¬A( ?x) V B(x)}

  • Move negation (¬) inwards as:

              ¬?x: A becomes ?x: ¬A and,

               ¬?x: A becomes ?x: ¬A

It means that the universal quantifier becomes existential quantifier and vice-versa.

  • Standardize variables: If two sentences use same variable, it is required to change the name of one variable. This step is taken so as to remove the confusion when the quantifiers will be dropped.

For example: { ?x: A(x) V ?x: B(x)}

  • Skolemize: It is the process of removing existential quantifier through elimination.
  • Drop universal quantifiers: If we are on this step, it means all remaining variables must be universally quantified. Drop the quantifier.
  • Distribute V over ?: Here, the nested conjunction and disjunction are flattened.

Example of FOPL resolution

Consider the following knowledge base:

  1. Gita likes all kinds of food.
  2. Mango and chapati are food.
  3. Gita eats almond and is still alive.
  4. Anything eaten by anyone and is still alive is food.

Goal: Gita likes almond.

Solution: Convert the given sentences into FOPL as:

Let, x be the light sleeper.

  1. ?x: food(x) ? likes(Gita,x)
  2. food(Mango),food(chapati)
  3. ?x?y: eats(x,y) ? ¬ killed(x ? food(y)
  4. eats(Gita, almonds) ? alive(Gita)
  5. ?x: ¬killed(x) ? alive(x)
  6. ?x: alive(x) ?  ¬killed(x)

Goal: likes(Gita, almond)

Negated goal: ¬likes(Gita, almond)

Now, rewrite in CNF form:

  1. ¬food(x) V likes(Gita, x)
  2. food(Mango),food(chapati)
  3. ¬eats(x,y) V killed(x) V food(y)
  4. eats(Gita, almonds), alive(Gita)
  5. killed(x) V alive(x)
  6. ¬alive(x) V ¬killed(x)

Finally, construct the resolution graph:

construct the resolution graph

Hence, we have achieved the given goal with the help of Proof by Contradiction. Thus, it is proved that Gita likes almond.

Note: There can be several examples of Resolution method in FOPL