Okay, can you hear me? Good. So, welcome back to AI. We're still doing propositional logic.

Remember propositional logic, that's the language we use to describe the world or no, we actually

assume our agents use to describe the world and its current state in. Our main kind of

running example is the wumpus world, where we're interested in things like, is there

a pit in square three four or something like this, or is there the wumpus there, because

we know about stench or glitter or those kind of percepts, and we know about general rules

of the game. If the wumpus is there, it stinks here, there, there and there and there. We've

developed and we've talked about, that was the main achievement last time, yesterday

actually, the main achievement was that we went from semantics, which tells us certain

things are valid, to syntax, namely purely formal means of ascertaining truth or entailment.

That's a, as I tried to convince you, big thing. There is by now a relatively large

research area called formal methods. That means we can do something about truth, in

this case mostly truth about my train control system will never in the future allow a situation

where there are two trains in one place going opposite directions or so. Those things we

don't really like. Program verification, protocol verification, all of those things are now

attacked by formal methods, because the semantics of nowhere in the future is daunting. The

future is long. If you want to do it in sufficient resolution, then you have to go down to the,

I don't know, sub-second level and then the next hundred years in sub-second level, that's

a lot of stuff to do. So you really want to be doing things at the formal level rather

than the semantic level. You're interested in the semantic level, you're interested in

the real world, that's what semantics is, that there is no two trains smashing into each

other. But you want to do something with pen and paper or Isabelle on silicon or something

like that. So there are systems, some of them use propositional logic, some of them use

other logics to do exactly that, to do what I called the miracle of logics. We looked

at various calculi, well actually two of them, no three, here's the third. We looked at this

Hilbert style calculus which has the wonderful property of being tiny and the terrible property

of oh how did Kohlhase have the idea of first writing down s twice and then k a couple of

times with funny substitutions so that c implies c comes out. You have this funny tendency

to start with big things and making them smaller and smaller and in the end doing the right

thing. And we looked at natural deduction which supposedly, and I think really, is actually

something that mimics how humans make proofs. That should really be better for algorithms

but has problems as well which we are going to look into and partially solve today. And

finally we looked at the sequent calculus formulation and the big step here and that's

something that those of you who ever want to do anything further with logic should probably

pay attention to even though it sounds trivial. Remember we graduated from search at the level

of states to doing reasoning at the level of world or state descriptions. Totally different

animal and in some cases more expressive or more efficient. Now in natural deduction,

for instance here, we are looking at the level of propositional formulae, taking a bunch

of formulae and deriving new formulae and we basically had in our mind what we're really

interested in going from valid to valid formulae or so. That works. But in many more advanced

cases that doesn't work so well. It doesn't scale as well. What we're now going to with

the sequent calculus is we're going to another level. We're going to the level of judgments.

The level of judgments is where we say oh we're not actually worrying about formulae

anymore but we're worrying about the judgments that if we can derive that we can derive that.

It's about derivations. We're doing derivation level reasoning now in the sequent calculus.

And actually if you think about it we were doing it all the time. With the ND proofs

it basically says well we wanted to find a theorem. We started out with a bunch of axioms

and the rule like a and b gives us a basically says if there is a derivation of a theorem

that starts with a and b I can actually find a derivation of a theorem. It's sufficient

to find a derivation of that. So we're really talking about derivations all the time. But