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
