Typing Description Logics Cheat Sheet
To help you type the Unicode characters, I’ve included methods for major operating systems, however I work on a Linux machine, so I can only say with certainty that the Linux method works. However, I did a little searching for you MacOS and Windows users and included the recommended methods here.
- Linux: press “ctrl” + “shift” + “u”, release and type the digits for the code after the ‘u’ character that appears, follow with a space to render the character. u2200 “space” will render ∀.
- MacOS: press “ctrl” + “cmd” + “space” to bring up the characters popover. Then type the code: U+2200 to find ∀, which you can include by hitting “Enter”.
- Windows: type “Alt” + “+” and then type the Unicode hexadecimal code (e.g., “2200”) followed by “Enter” to render ∀.
The Characters
| Symbol | Unicode | LaTeX | Description | Example | Read as | 
|---|---|---|---|---|---|
| ⊤ | 22a4 | \top | ⊤ is a special concept with every individual as an instance | ⊤ | top | 
| ⊥ | 22a5 | \bot | empty concept | ⊥ | bottom | 
| ∀ | 2200 | \forall | universal restriction | ∀r.C | all r-successors are in C | 
| ∃ | 2203 | \exists | existential restriction | ∃r.C | an r-successor exists in C | 
| ≡ | 2261 | \equiv | Concept equivalence | C≡D | C is equivalent to D | 
| ≐ | 2250 | \doteq | Concept definition | C≐D | C is defined to be equal to D | 
| ⊑ | 2291 | \sqsubseteq | Concept inclusion | C⊑D | all C are D | 
| ⊓ | 2293 | \sqcap | conjunction | C⊓D | C and D | 
| ⊔ | 2294 | \sqcup | disjunction | C⊔D | C or D | 
| ¬ | 00ac | \neg | negation or complement | ¬C | not C | 
| ⊢ | 22a2 | \vdash | proves or syntactic consequence | P⊢Q | Q is derivable/provable from P | 
| ⊨ | 22a8 | \models | satisfies | Q⊨S | Q satisfies all s for s in S | 
| semantic consequence | S’⊨Q’ | If all s in S’ is True, Q’ must be true. | |||
| ⊭ | 22ad | \not\models | negation of ⊨ | ||
| → | 2192 | \rightarrow | implication | C→D | C implies D | 
| ∘ | 2218 | \circ | composition | r∘s | s composed with r | 
| ⁻ | 207B | ^- | inversion | r≡s⁻ | r is equivalent to the inverse of s | 
| : | Concept assertion | a : C | a is a C | ||
| : | Role assertion | (a, b): r | a is r-related to b | 
Print It Out
I made the cheat sheet using Google Drive so you can view it and print it: Description Logics Cheat Sheet. I recommend keeping a copy next to your keyboard.
Until next time, happy typing.
Paul