dfkaye/symbolic-logic-entities.md

## symbolic-logic-entities.md

      
    Raw
  

              symbolic-logic-entities.md
            
          
    HTML entities for symbolic logic operators

See full reference at

Rapid Tables
W3Schools HTML Math entities.
Wikipedia List of Logic Symbols

Mathematical


+ - plus

HTML: &plus;
CSS: \002B


− - minus

HTML: &minus;
CSS: \2212


× - multiply

HTML: &times;
CSS: \00D7


÷ - divide

HTML: &divide;
CSS: \00F7


= - equals

HTML: &equals;
CSS: \003D


≠ - not equals

HTML: &ne;
CSS: \2260


< - less than

HTML: &lt;
CSS: \003C


> - greater than

HTML: &gt;
CSS: \003E


≤ - less than or equal to

HTML: &le;
CSS: \2264


≥ - greater than or equal to

HTML: &ge;
CSS: \2265


∘ - ring operator

HTML: &#8728;
CSS: \2218


∘ - composite function (e.g., sequential composition)

HTML: &compfn;
CSS: \2218


Propositional


∧ - conjunction (and)

HTML: &and;
CSS: \2227


∨ - disjunction (inclusive or ~ A or B or Both)

HTML: &or;
CSS: \2228


¬ - negation (not)

HTML: &not;
CSS: \00AC


⊻ - XOR exclusive or (A or B but not Both)

HTML: &veebar;
CSS: \22BB


⊕ - XOR exclusive disjunction (A or B but not Both)

HTML: &oplus;
CSS: \21AE


⊼  - NAND:

HTML: &#8892;
CSS: \22BC


⊽  - NOR:

HTML: &#8893;
CSS: \22BD


⇒ - implication (implies)

HTML: &Implies;
CSS: \21D2


⇔ - material equivalence

HTML: &hArr;
CSS: \21D4


⊤ - tautology

HTML: &top;
CSS: \22A4


⊥ - contradiction

HTML: &perp;
CSS: 22A5


≡ - equivalence (is equivalent to)

HTML: &equiv;
CSS: \2261


⊢ - assertion, proves

HTML: &vdash;
CSS: \22A2


⊨ - models

HTML: &vDash;
CSS: \22A8


′ - prime symbol

HTML: &prime;
CSS: \2032


Predicate


∀ - universal quantification (for all):

HTML:  &forall;
CSS:  \2200


∃ - existential quantification (there exists):

HTML:  &exist;
CSS:  \2203


≜ - delta equals (defined to equal):

HTML:  &trie;
CSS:  \225C


Set


∈ - membership (is element of):

HTML:  &isin; or &Element;
CSS:  \2208


∉ - not in
HTML: &notin;
CSS: \2209


∩ - intersection (element of S and T):

HTML:  &cap;
CSS:  \2229


∪ - union (element of S, T, or both):

HTML:  &cup;
CSS:  \222A


⊂ - subset

HTML:  &subset;
CSS:  \2282


⊃ - superset

HTML:  &supset;
CSS:  \2283-


⊆ - subset of or equal to (true iff every element of S is in T):

HTML:  &sube;
CSS:  \2286


⊇ - superset of or equal to (true iff every element of T is in S):

HTML:  &supe;
CSS:  \2287


∖ - difference (set of elements in S not also in T):

HTML:  &setminus;
CSS:  \2216


Temporal


□ - always, necessity:

HTML:  &square;
CSS:  \25A1


◻ - white medium square:

HTML: &#9723;
CSS: \25FB


⟡ - never; white concave-sided diamond:

HTML: &#10209;
CSS: \27E1


⋄ - eventually:

HTML:  &diamond;
CSS:  \25CA


◊ - eventually:

HTML:  &lozenge;
CSS:  \22C4


◇ - white diamond

HTML: &#9671;
CSS:  \22c7


≺ - precedes:

HTML: &pr;
CSS: \227A


≼ - precedes or equal to:

HTML: &#8828;
CSS: \227C


≾ - precedes or equivalent to:

HTML: &#8830;
CSS: \227E


↝ - leads to:

HTML:  &rarrw;
CSS:  \219D


⟼ - record construct:

HTML: &longmapsto;
CSS: \21A6


⟼ - xmap:

HTML: &xmap;
CSS: \27FC


∼ - stuttering equivalent

HTML: &sim;
CSS: \223C


↺ - backward:

HTML: &olarr;
CSS: \21BA


↻ - forward:

HTML: &orarr;
CSS: \21BB


Punct


❨ - left parenthesis

HTML: &#10088;
CSS: \2768


❩ - right parenthesis

HTML: &#10089;
CSS: \2769


❬ - left-pointing angle bracket

HTML: &#10092;
CSS: \276C


❭ - right-pointing angle bracket

HTML: &#10093;
CSS: \276D


✓ - check

HTML: &check;
CSS: \2713


✗ - cross

HTML: &cross;
CSS: \2717


Temporal logic properties

Taken from Standford U's Philosophy Dept. Temporal Logic article, specifically the section 11.1 Temporal logics in Computer Science.
Liveness


Liveness properties or eventualities involve temporal patterns of the forms Fp, q→Fp, or G(q→Fp), which ensure that if a specific precondition (q) is initially satisfied, then a desirable state (satisfying p) will eventually be reached in the course of the computation. Examples are “If a message is sent, it will eventually be delivered” and “Whenever a printing job is activated, it will eventually be completed”.

Safety


Safety or invariance properties involve temporal patterns of the forms Gp, q→Gp, or G(q→Gp), which ensure that if a specific precondition (q) is initially satisfied, then undesirable states (violating the safety condition p) will never occur. Examples are: “No more than one process will be in its critical section at any moment of time”, “A resource will never be used by two or more processes simultaneously”, or, to give more practical examples: “The traffic lights will never show green in both directions”, “A train will never pass a red semaphore”.

Fairness


Fairness properties involve combinations of temporal patterns of the forms GFp (“infinitely often p”) or FGp (“eventually always p”). Intuitively, fairness requires that whenever several processes that share resources are run concurrently, they must be treated ‘fairly’ by the operating system, scheduler, etc. A typical fairness requirement says that if a process is persistent enough in sending a request (e.g. keeps sending it over and over again), its request will eventually be granted.