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 ∀.
|⊤||22a4||\top||⊤ is a special concept with every individual as an instance||⊤||top|
|∀||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|
|:||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.