Inverting Resolution

• resolution rule - Robinson 65 - sound and complete
• this operator used in Cigol
• and
• any literal present in but not in must be present in
• the literal that occurs in but not in must be the literal removed by the resolution rule and therefore its negation must occur in
• or
• not deterministic! - so prefer shorter clauses
• Cigol uses inverse resolution with sequential covering but with 1st order representations