When entering expressions, use Ascii characters only. Use ~ for ¬; use & for ∧; use | for ∨; use => for ⇒; use <=> for ⇔; use A for ∀; use E for ∃; and use : for . in quantified sentences. Also, for variables use strings of alphanumeric characters that begin with a capital letter. For example, to write the sentence ∀x.∃y.(p(x) ∧ q(y) ⇒ r(y)∨¬s(y)), write AX:EY:(p(X)&q(Y)=>r(Y)|~s(Y)).