The right hand-side of a rule
You
can draw/complete the graph of the right hand-side of a rule. It
corresponds to element that will be added to your model in construction
during the execution of the tableau method.
Any extra variables
(in upper-case) are instanciated with new symbols. For instance
variable S will be instanciated in a new symbol s1, s2, s3... variable
PHI will be instanciated in a new symbol p1, p2, p3...
If you
want to compute something you need to "unquote" your expression by
using a comma. For instance, ,(+ 'N 1) will add the successor of the
number N (if N denotes a number!).