You may remember that I tried to convince you that peer grading of homeworks is a good

thing.

And then we failed to deliver.

It's been more difficult to implement than we thought.

We now have instructor grading, which basically means RTAs can actually grade your homeworks

that you submit.

Not that there were a lot of homework submissions, but there were some and we'll grade them.

And we'll probably hopefully get peer grading working over the Christmas break.

So that you can actually grade each other and that the whole thing scales.

Let me remind you that peer grading is not just us wanting to save work, but also just

turning the tables and seeing what other people do wrong is an immensely educational experience.

Just also like being on the other side of a hiring committee is interesting.

You learn a lot about yourself.

And so that is something you might want to try.

There was a question here.

No, there are no points.

But there's a good correlation between practicing and becoming good at something.

You can do that after the course in preparation for the exam or you can do it now while you

still remember what's going on.

But they have their advantages.

But no, homeworks do not give you any kind of bonus except the primary bonus of all studying,

namely learning.

Maybe the most important thing is they force you to think about the material again and

rub your nose in where you don't understand stuff.

Which is why I advise you to actually do them or at least look at them.

More questions?

OK, so what we did last time, last week, was we looked at calculi and procedures for automated

theorem proving.

The idea is that we have this satisfiability theorem that basically says if we want to

see whether a set age of hypothesis entail a conjecture A, then we can just as well show

that H together with not A is unsatisfiable.

Validity is the same as trying to make something false and failing completely.

That's the idea.

And even though this is a very, very simple trick, it actually gains us something, namely

a sense of direction.

We kind of think about the obviously unsatisfiable formula, the little closed branches and tableaus.

We're going to see another instance of this.

Then we have a goal we can work towards.

Whereas the goal of taking the hypothesis and finding the theorem A out there, that's

kind of a different target every time.

Makes it difficult to make heuristics.

But finding a contradiction is something that's always in the same place.

So we're going to see two...

Looks like I don't have power anymore in that device.

We're going to look at two calculi and I want to show them to you essentially back to back.

We're going to today look at the resolution calculus, which is a basically conjunctive

normal form based calculus.

And we've looked at the tableau calculus, which is a disjunctive normal form based calculus.

You can actually in this tableau you can see the conjunctions, every branch has a conjunction.

All of the things on the branch have to be true for the tableau to be satisfied.