I assume you can hear the microphone.

Good.

So we're still in logic land.

And we're looking at a logic called

ALC, which is somewhere between propositional logic

and between first order logic.

Ideally saying almost as much as first order logic

allows you to say.

In reality, slightly less, but hopefully so

that you won't even notice that we are retaining decidability.

And the prototypical logic here, like the mother

of all description logics is ALC.

That's what I want to essentially show you.

We've looked at the logic.

The logic is essentially first order logic

in its concept description code plus two guarded quantifiers.

Quantifiers that go over the R successors,

where R is a role like has child or is child of or whatever.

We looked at what the things are we can do with this logic.

We looked at concept definitions as essentially the things

we want to do with ALC at the level of the terminology.

And we looked at a direct semantics.

And we added the A box.

And that was very easy.

We basically have A as a member of concept phi,

and A is related to B under relation R.

And those two things allow us to do inference.

And I've shown you a surprisingly simple tableau

procedure, a tableau procedure that doesn't say,

this formula is valid, but basically has no A.

Basically has, we call them judgments of the form A box

judgments.

X is a member of concept C, or X is related to Y under relation

A, R. And with that, we can do inference in this logic.

The basic thing is satisfiability.

Is there an element to this concept?

That's important because we don't want

to talk about empty concepts.

And we've seen that this thing here is terminating, correct,

and complete.

Or in other words, give us a decision procedure

for satisfiability.

And all the other instruments, we

have to do for satisfiability, and all the other inference

things that we want to do, like classification and subsumption

and all of those things, can be played back

just like we did that in propositional logic

to satisfiability.

So satisfiability is the only kind of inference procedure

we need.