Enter a sentence in the window. To apply a transformation, click the corresponding button. If a dialog box appears, fill in parameters and press Transform. To enter selection mode, press escape to select the current expression. Select a subexpression using the arrow keys. Down selects the first child of the currently selected sentence. Left moves left across components, and Right moves right. Up moves to the parent of the currently selected component. To exit selection mode, press escape again. Pressing Undo also exits selection mode. When entering expressions, use Ascii characters only. Use ~ for ¬; use => for ⇒; use A 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.(p(x) ⇒ ¬s(x)), write the expression AX:(p(X)=>~s(X)).