Current Slide
Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.
Resolution  Principle

Resolution is a refutation system .

To prove a statement we attempt to refute its negation

Basic idea: Given a consistent set of axioms KB and goal sentence Q , we want to show that KB ⊧ Q

This means that every interpretation I that satisfies KB also satisfies Q

Any interpretation I only satisfies either Q or ¬ Q, but not both

Therefore, if in fact KB ⊧ Q holds , an interpretation that satisfies KB , satisfies Q and does not satisfy ¬ Q

⇒
Hence KB
∪
{
¬
Q
}
is unsatisfiable, i.e., it is false under all interpretations