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.