Good. Tableaus is one way of doing it. There's another way of doing it using

what we call the resolution calculus. And this has a single inference rule namely

we have a language where we only have disjunctions of literals. P true, Q

false, or, or, or, or. We have only one rule which makes it very easy to implement by

the way. That says well if you have two formulae, P true or A, P false or B, then

I can derive A or B. Or you can think of this if I find two contradictory

literals, then I can cut on them and just look at the rests. Okay? And what am I

looking for? I'm looking for a contradiction. And the contradiction in

this case where we only have disjunctions of literals is the kind of

extreme case. So if you think about disjunctions of literals and think about

how easy it becomes to make them true, then you can see that the more literals

you have, the easier it becomes to make them true. Right? If I have P, then I must

make P true to make this thing true. If I have P or Q, then I can decide to make

either P true or Q true. So the shorter the literals become, the shorter these

things we call them clauses become, the more difficult it gets to make them true.

And when you don't have any literals left over, then you can't make it true at

all. Okay? So the empty clause is kind of, if you will, the empty disjunction.

And that's what we're looking for as a contradiction. We're doing it exactly

like we're doing it for the tableaus, only where we kind of did a

development in a tableau with all the closed branches. Beforehand, we start with

a formula set, a clause set, in this case, we do resolution, resolution, until we

find an empty clause. Where is an example? Yes. Here I have an example. Say we have

P false or Q false or R true, and another clause P false or Q true, and a P true

and an R false, four clauses, all of them are disjunctions of literals. Then I can

actually start resolutions. So for instance, I can, I see that I have an R

true here and an R for here, so I can resolve this against that and collect up

the rests. Here's no rest, there is the rest P false or Q false, right, which is

the new clause. Now I can see I have a P false here and a P true there. I can cut

on those two, collect up the rests, there's only one Q false, which is the

rest. Now I can go back, there's a Q false here and a Q true there, collect up the

rest, gives me a P false, and I have a P true here and a P false, collect up the

rests, there are no rests, so we have an empty clause. Okay, very simple calculus, very

very easy to implement. Just think of these formulas as lists of

literals. So a clause set is nothing as a list of lists of literals, which is

something very very easy to implement in any programming language. The only thing

you need to do is resolution, look for complementary literals, cut and go on.

Until you have the empty list as an element of the list of all clauses you

have, boom you're done. Now that's resolution, that's the idea of resolution.

The problem with resolution is that you can only do it for things like this,

which are formulae that are clauses where you have a set of clauses or a list of

clauses if you want, and clauses are just very very special formulae. Now we know

that any propositional formula I can transform into a clause set, and I need

four rules for that. Whenever I see a rest or a or b true, I transform that into a

clause c or a true or b true. If I see a c or a or b false, then I split that into

two clauses c or a false, c or b false, and I have two

negation rules. If I see a rest and not a true, then I make an a false out of that.

You can already see here that certain connectives, that in every

case, kind of the scope of the label decreases. So this is going to be a

terminating thing. It's going to terminate, same argument again, right? I have a

measure, I'm counting kind of the, I'm counting the overall scope of connective,