Resolution

• Resolution is a valid inference rule producing a new

clause implied by two clauses containing
complementary literals
– A literal is an atomic symbol or its negation, i.e., P, ~P
• Amazingly, this is the only interference rule you need
to build a sound and complete theorem prover
– Based on proof by contradiction and usually called
resolution refutation
 What is Resolution in First-Order Logic

• A resolution is a rule in first-order logic (FOL) that

allows us to derive new conclusions from
previously established data. According to the
concept of proof by contradiction, if assuming
something is incorrect results in a contradiction,
the assumption must be true.
• The resolution approach is widely employed in
logic-based problem solving and automated
reasoning because it produces systematic,
thorough, and efficient proofs of logical
statements.
• A KB is actually a set of sentences all of which
are true, i.e., a conjunction of sentences.
• To use resolution, put KB into conjunctive
normal form (CNF), where each sentence
written as a disjunc- tion of (one or more)
literals
 Why Do We Use Resolution
• Prove Statements Logically Resolution uses
contradiction to assess if a statement is true or false.
• Automate Logical Reasoning - Allows computers to
automatically draw conclusions from provided facts.
• Solve Problems in AI and Logic Programming - Used in
Prolog and other AI applications for rule-based
reasoning.
• Ensure Consistency in Knowledge-Based Systems -
Assists in detecting inconsistencies and maintaining
valid information.
• Verify Software and Systems - Ensures that software,
security protocols, and hardware are working
properly.
 Key Components in Resolution
• Clause
A clause is a dis-junction that serves as a fundamental unit in resolution-based proofs. Following are
the examples to better understand the Clauses −
P(x)¬Q(x) → This expression consists of two literals linked by OR ().

• Literals
A literal is either the atomic proposition (fact) or its negation. Literals are the building blocks of
clauses. Here is an example of literals.

• Unification
Unification is the operation of two logical expressions by determining the correct substitutions for
the variables to make both expressions equal. Here is an example of Unification.

• Substitution
Substitution is the replacement of variables by definite values or words in a logical formulation for
more specific expression. It is used in unification, resolution, and inference rules to make logical
assertions more specific.

• Skolemization
Skolemization is the process of removing existential quantifiers () by introducing Skolem functions or
constants.
 Steps for Resolution in First-Order Logic (FOL)

The resolution process involves systematically modifying logical statements and utilizing
unification and resolution principles to either derive a contradiction or establish the
desired outcome. Below are the key steps involved in FOL resolution −

• Convert statements to First-Order Logic (FOL) and express the given information
using FOL notation.
• Convert FOL sentences into Clausal Form (CNF) by removing implications, moving
negations inward, standardizing variables, applying Skolemization, and converting to
conjunctive normal form.
• Negate the assertion to be verified - Assume the negation of the goal and include it
in the list of clauses.
• Apply Unification: Find relevant variable substitutions to make literals identical.
• Use the Resolution Rule: Identify complementing literals and resolve them to create
new clauses.
• Repeat until a contradiction or proof is found. Resolve until an empty clause () is
derived (contradiction) or the goal statement is proven.
 Working of Resolution Algorithm
The Resolution Algorithm works on clauses that are small logical statements connected by "AND" or "OR." It
works by:

Step 1: Convert Statement into Logical Forms

First, input sentence is converted into a standard format called Conjunctive Normal Form (CNF) means we
break down the complex statements into simple parts connected by "AND" and "OR."
If the Original statement: "If it is raining then the ground is wet." then its CNF is: "NOT(Raining) OR Wet.

Step 2: Combine Clauses Using Resolution Rule

The core idea of the Resolution Algorithm is the resolution rule which combines two clauses to produce a
new clause.
If you have two clauses say A OR B and NOT(A) OR C you can combine them to get B OR C. This process
eliminates one variable (A in this case) and simplifies the problem.

Step 3: Repeat Until You Find an Answer

The algorithm keeps applying the resolution rule to pairs of clauses until one of two things happens:
Contradiction Found : If the algorithm produces an empty clause (written as FALSE) it means the original set
of statements is inconsistent and cannot be true at the same time.
No Contradiction : If no empty clause is found after trying all combinations then the statements are
consistent and can coexist..
 Examples of Resolution in AI
Resolution plays a crucial role in various AI applications as it enables
automated reasoning and logical inferences. Here are some key
examples of how resolution is applied in AI.
• AI has an impact on Automated Theorem Proving - Resolution to
prove mathematical theorems without human intervention..
• Expert Systems - AI systems use rule-based reasoning to draw
logical conclusions. In medical diagnosis, expert systems like
MYCIN use resolution to guess diseases based on symptoms and
patient information.
• Natural Language Processing (NLP) - Resolution helps to break
down and show meaning. AI-based NLP models such as IBM
Watson and Google's BERT, apply resolution methods to find
logical connections between words and boost language
understanding.
• Knowledge Representation : In AI systems knowledge is
represented as logical statements. The Resolution
Algorithm allow these systems to reason about that
knowledge effectively.
• Problem Solving : Many real-world problems can be framed
as logical puzzles. For example scheduling tasks, diagnosing
faults in systems or planning routes can all benefit from
logical reasoning using resolution.
• Foundation for Advanced Techniques : The Resolution
Algorithm forms the basis for more advanced AI techniques
such as SAT solvers which is used to solve Boolean
satisfiability problems and logic programming languages.
 Limitations of Resolution
Below are some key limitations of the resolution
method in logical inference
• Computational Complexity: It produces
numerous intermediate clauses, making it slow
when dealing with large knowledge bases.
• Lack of Expressiveness: Transforming to CNF
limits the expressiveness of some logical
propositions.
• Handling Infinite Domains: There are challenges
with recursive definitions and infinite problem
sets.
• Efficiency: The algorithm can be computationally
expensive due to the large search space,
especially for complex systems.
• Requires CNF Conversion: Every logical formula
must be converted to CNF before applying the
algorithm which can be time-consuming.
• No Direct Answer: The resolution algorithm works
through refutation meaning it doesn't construct a
solution directly but rather disproves the negation
of the goal.
 Conclusion
• Resolution is inherently monotonic, which
means that once facts are introduced, they
cannot be removed. This characteristic makes
it unsuitable for managing dynamic or
uncertain knowledge where conclusions might
need to be adjusted.