This is an old revision of the document!
Exercises 04
Example resolution proof.
Constructing interpolants for this case.
Continuation of correctness proof for interpolant construction from resolution proof.
Running DPLL on the example.
Menu