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.