Description Logic and Question 4 in Project 1

[peihongx]

@johnbeve Hi John,

We classmates had very cool discussion of definitions in description logic (DL) today. But I have some doubts about syntax of DL:

(1) Ali and Giacomo told me that you said that parent_of is a primitive and is not defined as anything, so its reverse could technically take any value. Using the inverse of parent_of directly is not possible to be defined since we need a direct definition of parent_of in first place. But if we assume parent_of, we can define inverse terms that use parent_of indirectly. For example, they defined:

p2 (parent of at least 2 children) := (∃parent_of. ≥ 2),

and then defined its inverse p2- (meaning: x be one of at least two children produced by y).

My question is, why can't we directly introduce the inverse of a primary role name like parent_of if we can introduce the inverse of a non-primary role name like p2? It sounds so weird. Ok, Baadar's book talks about a similar example (p. 38): taught_by is not the inverse of teach (a primary role name) but another arbitrary role name. But then Baadar immediately introduces teach- as the inverse of teach and says that taught_by can be the inverse of teach if it is just teach-. So why can't we similarly introduce parent_of- as the inverse of parent_of directly?

(2) Ok, I pretend that I follow Ali's and Giacomo's approach, then I can define a new role name like:

p1 (be a parent of at least one child) := (∃parent_of. ≥ 1), and then define its inverse p1-. Here p1- means "x be one of at least one child produced by y", that exactly is, "x be a child of y"!

In this way, we indirectly go through p1- to the inverse of parent_of, which is actually parent_of-. So if the inverse of a primary role name cannot be directly introduced, then we can indirectly but uglily do the same thing. But is DL really so ugly?

[johnbeve]

Hi @peihongx,
Regarding (1): parent_of is primitive, but I didn't say the inverse could take any value. What I said was that you couldn't simply define the inverse of parent_of - call it "has_parent" - as:

x has_parent y =def y parent_of x.

I wanted students to think harder than that; hence the restriction. In practice, inverses for primitive relations are frequently introduced. See here and here. That aside, p2 isn't the inverse of parent_of, so what I said to @giacomodecolle and Ali doesn't apply. Defining p2- is fine by me.

Regarding (2): p1 would address the constraint I raised, since it is a definition for parent_of, and so you're welcome to define an inverse. This seems ugly in part because I'm requiring that if you define a direct inverse of parent_of, then you need to define parent_of.

[peihongx]

@johnbeve Thank you so much! Now I know that it is practically viable to directly introduce the inverse of a primitive role name, but here we have to deal with a bigger challenge for the purpose of education! That makes sense a lot!