17 lines
368 B
Plaintext
17 lines
368 B
Plaintext
|
Resolution
|
||
|
|
Examples
|
||
|
|
Soundness of resolution rule.
|
||
|
|
|
||
|
|
Res*(F)
|
||
|
|
|
||
|
|
Proposition 1:
|
||
|
|
If \emptyset \in Res*(F) then F is unsatisfiable.
|
||
|
|
Proof : (by contradiction and using soundness of resolution rule)
|
||
|
|
|
||
|
|
Proposition 2:
|
||
|
|
If F is unsatisfiable then \emptyset \in Res*(F)
|
||
|
|
Proof : (by induction on #prop_variables appearing in F
|
||
|
|
Base case : when F has only one variable.
|
||
|
|
|
||
|
|
|