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
