Okay

so quiz is over.

We're talking about a world description language

aka a logic called ALC.

The idea there is that we try to kind of get as much functionality

expressive functionality

out of first-order logic without crossing the decidability line.

And the main mechanism here is that we basically have a funny variant of quantification

something

of the form for all r phi

where phi is a concept and r is a relation

which really

means

and correspondingly

and this actually means

so later in the tableau

x is a member

say there is r phi

that really means that x has an r successor that is in phi.

And the intuition here is that instead of the first-order formula for all xA

which

really says all of the x's in the whole universe

which may be extremely many

have the property

of making A true.

Here we're basically saying something about for all or exists

but only for the r successors.

And you can imagine that the set of r successors is kind of systematically smaller.

And that's the difference between these two logics.

We can say for all x's in the universe

of which there are more

and for all r successors

is kind of a restricted quantification

that's smaller.

And that's really the thing that makes this decidable.

And we've looked at

we started looking at

the satisfiability problem using a tableau

algorithm for two kinds of judgments.

One is x is in a concept phi

and x is r related to y.

Those are the things we put up in our calculus

and that gives us this very simple little

calculus.

We have a closure rule that if something is in a concept

an atomic concept

and it's

a complement

then you can close the and and the rules for intersection and union behave

exactly like and and or.