**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