Formal Description Logic - mdebellis/SemanticKG-Design GitHub Wiki

The language I use in the book to define axioms is called Manchester Syntax. I’ve been calling it Description Logic, but the more formal name is Manchester Syntax because there is an actual formal language called Description Logic, or DL for short. Now, if you're math-phobic, don’t worry. You don’t need to use this formal language in day-to-day work with OWL ontologies. But you will see it now and then in books, documentation, and papers. When you do, the table below will tell you what each symbol means.

At its core, Description Logic is just another way to describe the same ideas we’ve already learned: classes, properties, relationships, and logical constraints. But instead of using the user-friendly Manchester Syntax such as:

Animal and (not (Human)) and ('is pet of' some Human)

Description logic uses symbols from logic:

Animal ⊓ ¬Human ⊓ ∃is_pet_of.Human

The specific DL symbols in this example have the following meanings:

• ⊓ = intersection (logical AND)
• ¬ = negation (logical NOT)
• ∃R.C = existential quantification, i.e., "there exists some instance of C such that value of the R property is the object of the thing we are defining"

The Description Logic formalism comes from logic and knowledge representation research. It gives a precise foundation for what OWL can express. You can think of it like this: Manchester syntax is for people who want to build ontologies. DL syntax is for people who want to talk with mathematical precision about what OWL can express. In order to keep the table in a readable font, I use CamelCase rather than my normal Underscore_Case. The following table shows the DL symbols, examples from the People ontology in DL, what they mean in plain English, along with their Manchester Syntax equivalents. You don’t need to memorize these, but you may come across them, so it is good to have a “cheat sheet” to refer to if you need it.