Hello I am new to description logics and ALC and I find it confusing defining a KB. More specifically I am trying to create an ALC KB for the first 3 sentences below and an ALC formula φ that formalizes the last one.
Sentences:
• Anna is a person.
• The only kind of coffee that Anna drinks is latte.
• A French is a person who drinks only latte coffee.
• Anna is French.
My KB so far:
TBox T:
French ≡ Person ⊓ ∀drinks.Latte
Abox A:
Person(ANNA), drinks(ANNA, LATTE)
φ: French(ANNA)
My questions are:
Is it wrong that I considered latte as concept or I should have written ∀drinks.Coffee instead, because coffee could be considered also a concept?
Is the assertion drinks(ANNA, LATTE) redundant because in the Tbox ∀drinks.Latte exists?
Any suggestions would be appreciated. Cheers!
I think you can model Person
, French
, Coffee
and Latte
as concepts with the following axioms:
French ⊑ Person
Latte ⊑ Coffee
The axiom French ≡ Person ⊓ ∀drinks.Latte
may be problematic. The reason being that the reasoner will infer whenever an individual x
is a Person
and x
only drinks coffee, that x
is French
. But it is completely possible that there are people who only drink only lattes but they are not necessarily French. For that reason it is better to express it as follows:
French ⊑ Person ⊓ ∀drinks.Latte
If you now have ANNA
as an individual and you assert French(ANNA)
, this is sufficient. I.e., the reasoner will "know" that ANNA
drinks only lattes. However, if you do this in Protege (for example), the reasoner will not infer that ANNA
only drinks lattes. The reason for this is that ANNA
is in essence an instance of the complex concept expression Person ⊓ ∀drinks.Latte
, because we said she is French. Reasoners give inferences in terms of named concepts only because in general there can be an infinite number of inferences in terms of complex concept expressions.
To see that the reasoner "knows" this. Create another sublass of Coffee
class, say Expresso
that is disjoint with Latte
. Create an instance of Expresso
, say EXPRESSO
and assert drinks(ANNA, EXPRESSO)
. Running the reasoner now will cause an inconsistency.
As for your question regarding modeling Latte
as concept or an individual: usually it is better to model as a class. I explain this for OWL in this SO question. This holds to true for ALC as well.
If you want understand more about when to use equivalence versus subsumption, I have written about this on my blog here.