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.