The left hand-side of a rule
To
edit the left hand-side of a rule, you can draw with the mouse the
pattern of the graph that has to be matched in the model in
construction during the execution of the tableau method.
Variables for pattern-matching are written in upper-case. All formulas etc. are written in a Scheme way.
You
can add extra-conditions for pattern-matching. For instance, if you
want your variable P to denote any propositions yo ucan add:
(proposition? P) in the condition box.