=================================================================================

Resolution is a powerful inference rule used in propositional logic and first-order logic to derive new clauses from existing ones. In automated theorem proving, resolution is often employed in proof methods such as the Resolution Refutation. The basic idea of resolution is to resolve two clauses by finding a complementary pair of literals, one positive and one negative, and then resolving or eliminating them. The resolution step results in a new clause that combines the remaining literals. The resolution rule can be formally stated as follows: 

Suppose we have two clauses:

where ,

P is a literal.

¬P is its negation. 

The resolution of C₁ and C₂ is the clause: 

where,

         Res(C₁, C₂) is obtained by removing both P and ¬P from C₁ and C₂ and combining the remaining literals.

Resolution is often used in automated theorem proving to show the unsatisfiability of a set of clauses. The process involves repeatedly applying the resolution rule until either a contradiction is derived (e.g., an empty clause), indicating the unsatisfiability of the original set of clauses, or the process cannot proceed further. 

============================================