


          Welcome to xmagic 0.9.

               Xmagic is a windowing interface to John Slaney's MaGIC.
          Xmagic  has been written at the Automated Reasoning Project,
          The Research  School  of  Social  Sciences,  The  Australian
          National University, by Gustav Meglicki.

               Xmagic provides a control panel which  enables  you  to
          operate MaGIC by pushing buttons and setting switches.

               Xmagic can be set up in such a way that MaGIC  will  be
          executed  on  a remote host rather than on your own worksta-
          tion. This is a preferred way to run the  "MaGIC  -  xmagic"
          combination,  in  particular  if you intend to work on large
          and difficult problems.

               When xmagic starts up you are presented with  the  main
          control  panel. You can select the type of logic you want to
          work with by clicking on one of the  choices  in  the  logic
          box. Likewise you can select various other parameters of the
          job you want to submit to MaGIC: order,  fragment,  type  of
          output, etc.

               On the right hand side of the control pannel  you  will
          find four dialog boxes labelled: "fail on formula", "maximum
          number of matrices", "maximum size of matrices",  and  "stop
          when  time  exceeds".  All these boxes are disabled. You can
          activate them by clicking on the "on" label  situated  under
          each  of  the  dialog  boxes. You can disable the boxes (and
          also the corresponding  action  they  would  carry  out)  by
          clicking  on  the  "off" label. If you enter anything in the
          dialog box, you must click on the  "change"  button  if  you
          want the information in the box to be sent to MaGIC.

               You can use standard keyboard bindings  of  the  Athena
          text  widget, while manipulating text in all dialog boxes of
          xmagic. The most useful are CTRL-K, which will delete every-
          thing between the cursor and the end of the line; and CTRL-W
          which will delete a selection.

               On top of the control panel there is a switch with  two
          positions  labelled "silent" and "verbose". If the switch is
          set to "verbose" you get to see everything  MaGIC  sends  to
          xmagic  in  the  window underneath the control panel. If the
          switch is set to "silent" only the information asked for  by
          settinng  the  "tty  output"  switch  is  displayed. You can
          scroll back and forth through the displayed text  using  the
          scroll bar on the left hand side of the display window.

               If you press on the "add axioms" or "connectives"  but-
          tons  a  new  window will appear which will allow you to add
          predefined axioms and define the new ones, or to define  new
          connectives.

               Once you've set up all the job parameters to your  lik-
          ing  press  a button in the bottom part of the control panel
          labelled "go".  You should then see the results of the MaGIC
          job appear in the display window.

               If at any stage you send an incorrect input  to  MaGIC,
          an  error  message will appear in the display window and the
          action will be disregarded.

               Notice that xmagic  will  not  be  responding  to  your
          inputs  while MaGIC is running the job. The "stop" button is
          not implemented yet, although it has been already placed  in
          the  control  panel. Once MaGIC has finished the run, xmagic
          will again accept your input. You can either  submit  a  new
          job  (you  can  press  the "reset all" button to set all the
          settings to what they were at the  beginning),  or  you  can
          quit xmagic and MaGIC by pressing the "quit" button.
