# Resolution in Artificial intelligence

Resolution method is an inference rule which is used in both Propositional as well as First-order Predicate Logic This method is basically used for proving the satisfiability of a sentence In resolution method

## Resolution 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

## Example of Propositional Resolution

Consider the following Knowledge Base:

• The humidity is high or the sky is cloudy.
• If the sky is cloudy, then it will rain.
• If the humidity is high, then it is hot
• 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:

• Let, P: Humidity is high
• Q: Sky is cloudy.

It will be represented as P V Q.

• Q: Sky is cloudy
• Let, R: It will rain

It will be represented as bQ → R

• P: Humidity is high
• Let, S: It is hot