So resolution, if we are in conjunctive normal form or clause normal form, then we can get

to an empty clause which is the contradiction here by using just one rule.

You have two clauses which are disjunctions of literals and if you see a complementary

literal you can cut it out, concatenate the two rests, add that.

Soundness here is obvious.

Anybody care to make an argument for soundness here?

Soundness has something to do with meaning.

Meaning has something to do to giving true or false to propositional variables.

Now P can have two values.

If P is true, then this whole thing here must be true.

But then this literal is certainly not true.

So not satisfied.

So to make this true you have to satisfy the rest of B. Make one of those true.

Which is enough to make that thing true.

That's the true case.

Or it could be false.

Well then this here is not satisfied so one of the literals in A has to be satisfied.

Which is enough to make this satisfied.

And here this is already true and so the rest doesn't matter.

That's soundness.

Easy peasy.

Completeness, different story, look at the back of the notes.

So the only thing we still have to learn is how to make something into clause normal form

and we can do so by four simple rules that don't look that different from the tableau

rules except that this is kind of the not the disjunctive normal form way of computing

but the conjunctive normal form of computing.

And indeed this calculus, these four rules actually turn everything into clause normal

form.

Right?

Because clause normal form, disjunctions of literals is the only way where we cannot apply

one of these rules.

These rules always have disjunction under a true and we pull it in.

And when we're at the literals we stop.

Okay.

There's one little wrinkle I want to also allot you to.

I said when we have a calculus we're interested in three things.

Soundness, completeness and termination.

Sometimes we're also interested in something else.

Which this gives me a very nice example.

In a calculus we want to kind of search for all proofs, for all theorems, which means

all provable things so I have to search for all proofs.

Then we're looking in the space of all proofs.

So I have to systematically enumerate all proofs to see whether I reach where I'm going.

Whenever we have possibilities that's in search.

Whenever we don't know what the right path is we have to look at all of them.

Sometimes we're in a situation where the path doesn't matter because I can show that all

the paths lead to the same solution.

You may have heard that all paths lead to Lhasa and all roads lead to Rome.

And if you want to get to Rome you just follow all the streets.

It will get you there eventually because all streets go to Rome.