Xmagic allows you to type in formulae in three places:

          1    in the "bad guy" window: this is the top  right  dialog
               box on the main control panel;

          2    in the "define axiom" pop-up window: this window can be
               called from the "add axioms" pop-up;

          3    in the "connectives" window.

               The following conventions govern typing of formulae:

          a    Variables are  'p', 'q', 'r', 's'.  Upper case will  be
               converted  to  lower  by  the parser.  Any other letter
               will be treated as garbage.

          b    Parentheses should be written in full, except that

               i    outermost parentheses are unnecessary

               ii   all right parentheses are unnecessary

               iii  a period (".") is equivalent to "("

               Because no scope rules are in force, association to the
               left  is  assumed.   Therefore the right mate of a left
               parenthesis immediately follows the shortest  interven-
               ing formula with dyadic main connective.  For this rea-
               son right parentheses are redundant.

          c    Spaces are ignored.  RETURN terminates the formula.

          d    The connectives are "&"  (ampersand),  "v"  (vee),  "~"
               (tilde)  and  ">" (greater than).  Implication may also
               be written as "->" (with optional  minus).   Sentential
               constants "t" and "f" are also allowed.