# Typing Description Logics Cheat Sheet

29th April 2018Many of the unusual symbols we use when writing Description Logics are sadly not found on the keyboard. I wrote myself a little cheat sheet to remind myself of the correct unicode or LaTeX for the common symbols and added a short description of each symbol as well. It's very useful to print out and keep near your keyboard so you can type Description Logics quickly and painlessly.

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 for you.

**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 the code. “Alt +2200” will render into ∀.

## 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