Logic & Inference

Inference through Resolution

Proof by refutation: convert to CNF, negate the goal, and resolve clauses until the empty clause appears.