That gives us soundness and correctness.

The last thing I want to briefly show you is termination.

And here the termination is a little bit more difficult than the termination for the propositional

tableaux.

So we're in the propositional tableau case, which is basically this case here.

This case here that we look at is the propositional case and we add two rules so termination is

more difficult.

So the thing to realize here is that every rule except the for all rule can only be applied

once to a particular x colon psi.

That was what we realized in the case for propositional tableaux.

And this is also the thing that ruined termination.

Remember the multiplicity in tableaux, in first order tableaux, that actually ruined

decidability for us in the case.

The thing here is that even though we can apply the for all rule multiple times, we

can still control how often it is applied by looking at the second thing it needs.

It needs these x,r,y's and we can see where might they come from.

Well they're not coming from one of those, that's clear.

So they must come from an existential.

So the critical thing is we work on an existential once and then we can actually, then we can

actually again make a new application of the for all.

Remember in our examples here, we had a for all here which we couldn't apply until we

had worked on the existential which had given us an x,r,y.

Now that we have the x,r,y we can apply the for all.

And that's the general thing.

We can only apply the for all if we have an x,r,y and the x,r,y can only come from an

existential.

Now if we count the number of existentials we know actually how many x,r,y's are going

in to be in here.

Like no existential, ah there's an existential so there we would predict that there's only

one x,r,y in here.

And indeed there is only one x,r,y which allows us to predict that this thing here, the for

all, the number of for all actually are triggered exactly once.

And that will, that gives us the termination.

So any rule except for all can only be applied once.

C for all is applicable to x for all, r,psi at most, the number of r successors of x.

And the r successors are generated by an existential and so the number is bounded by the size of

the input formula and so we get the termination result.

Everything gets smaller.

This is the good news.

This proof is actually why ALC is an interesting logic at all because we know that it has a

decision procedure.

Once you, once you look at termination of course you want to have the complexity and

the idea is that we can get an upper bound on the complexity by looking at this tableau

procedure we work off one of the branches after the other.

And we see that the size of the branches is polynomial in the size of the input formula.

If you look at this idea of every existential giving one rule here, then you can see that

the size of the input formula matters.

That gives you how many rule applications at most you get and then you have an extra

number of rule applications for the existentials and the universals.

So you just have to take the, take the sizes of those, the numbers of existentials and