Good. So this actually lets us progress to satisfiability tests. We have the semantics

so we can actually define what satisfiability means. And we're going to look at a particular

class of algorithms which has become the relevant part, the best fitting to inference in description

logics. Basically, all the algorithms that are used for inference are tableau-like algorithms.

So remember, a tableau kind of takes a formula or a set of formulae and develops that into

a tree-form scheme using these tableau extension rules, then we're always looking for saturated

tableaus where new rules are applicable. So a saturated tableau where all the branches

are closed, i.e. end in this funny nail-like symbol, the bottom symbol is a refutation.

And so the formulae in the calculus aren't a labelled formula of the form A true or A

false, but we just directly take the assertions. And then we have tableau rules that are really

quite simple. If we are in a situation where X is in a concept C but also is in its complement,

then this of course cannot be, so this is a source of inconsistency. If X is in the

intersection of phi and psi, then it's in both phi and psi. If X is in phi or psi, then

we have that is either in phi or in psi. And if we have an X that is in for all r phi,

and we also know that Y is an r successor of X, then we can conclude that Y is in phi

because we know that X is in a concept where all the r successors are in phi, so we conclude

that Y is in phi. And if we know there is an r phi, then we conclude that a new object

Y and then we have to prove that Y can actually be in phi. So if we want to test the concept

consistency of a concept phi, we normalize phi to psi. Remember normalizing gets rid

of all the definition. Then we initialize the tableau with X psi. We saturate, and if

there are open branches, then this is consistent. Remember in the tableau, we always had open

branches directly gave us models. By the way, which X we take to initialize the tableau

doesn't really matter. We could take anyone. So this assertion, there is an X that is in

phi is really what we want. We want to show that a concept is consistent, i.e. nonempty,

not false, if you will, in the DL framework. So let us look at two examples. One is we

look at the concept that says all of the children are men, and there is a child that is not

a man. This should be inconsistent. You can't have only male children, but also have a non-male

child. But we have a consistent example here. All the children are male, and there is indeed

a male child. And we're going to do the tableau proof here. We're trying the first here on

the left. We try this one. So we have an X that goes, that is in an intersection that

actually gives us two, namely this one and that one. From the for all, no, from the exists,

we can find, we can see, where's mine, right? The exists actually gives us an R successor

that is in phi. So here we're getting a Y that is an has child successor to X. And we

postulate that this Y successor, that this Y is, where is it from? Well, from the complement

of man, we now have an X with a for all has child man, and we have an X has child Y, which

is exactly the situation we need in this rule here. So we can conclude from that that Y

is in phi, which here is Y is in man. So that's what we do from line number two. And then

we have an elementary contradiction. So since we don't have any other branches, this thing

here is inconsistent. The situation is different if we, in the second example, there we have

for all has child man and exists has child man. So no compliment here. So we do exactly

the same thing. We split the two concepts in the intersection. We do the existential

X has child Y, Y is a man. But this here for all has child man, which we can apply to find

out that Y has man. So this does not add anything to the tableau. So we leave it out in the

situation, and there's nothing we can do. So we have an empty branch. And if you look

at that, that model, the model for X being in this concept is there being a child of

X, Y, that's male. So in the model in the right, we have two persons, X and Y, Y is

the only child of X and Y is a man. That's how the tableaus work. Let's do it. Let's

do a bigger one. So we have a concept of all the objects that are children that have children

that are undergrads or graduates, and that also have a child that is not an undergrad.

Let's see whether that is satisfiable. Usually I would do this on the board. Here I'm going