resolution-method

Resolution is a theorem prover method which is sound and complete. It works by converting the premises and conclusions to clause expressions or clausal form.

What resolution method says is,

$$\frac{\{\neg p,q\},\{p,r\}}{\{q,r\}}$$

It means, if two clauses having a literal and its negate, then we can combine all those clauses by removing those complementary pair.

$$\frac{\{p_1,p_2,...,p_n,\neg q\},\{r_1,r_2,...,r_n,q\}}{\{p_1,p_2,...,p_n,r_1,r_2,...,r_n\}}$$

Important

Empty clause means that the set of clauses are unsatisfiable. This property will be used one the applications (proving the unsatisfiability).

Common Resolutions

1. Modus Ponens

$$\frac{p\to q,p}{q}$$

This is can be done using resolution method.

$$\frac{\{\neg p,q\},\{p\}}{\{q\}}$$

Reference

1. Propositional Resolution