Definition
Resolution Inference Rule (Propositional Resolution)
where
is called the the resolvent and is called resolved atom.
Examples
Example
Given a Boolean function in CNF:
The unit clause is
. Find all clauses that contain , the complement of :
, then the resolvent is , then the resolvent is , then the resolvent is , then the resolvent is From there, we continue:
and , then the resolvent is and , then the resolvent is The resolvent of
and is an empty clause. If an empty clause is found, then the Boolean function is unsatisfiable:
Example
Example