How to use SPASS and Isabelle

hets -g Resolution.casl

and klick on a node (Regen, Logolei) with with right mouse button. Select the "Prove" menu. Then select the goals that you want to prove, and the prover:

• SPASS:If you have choosen SPASS, initially, all selected goals are tried in a row. After this so called batch mode the results are displayed in a window which is shown in Fig. \ref{fig:SPASS_GUI}. This GUI for the theorem prover SPASS is very similiar to the 'Select Goal(s) and Prove' GUI which lets you choose a prover for some goals. But with the SPASS GUI, the actual SPASS prover is launched with the selected goal. Further it is possible to set a time-limt and some options for SPASS. The available options are shown in separate window by pressing the 'Help' button. The status of the selected goal is shown in the 'Status:' line with either 'Proved', 'Disproved', 'Open' or 'Open Time (Time is up!)'. If a goal has been proved the labels of the used axioms are shown in the list on the right. The button 'Show Details' shows the whole output of SPASS. 'Save Prover Configuration allows you to save the configuation and status of each proof for documentation. By pressing the button 'Exit Prover' the status of these proofs and goals is transferred back to the main 'Select Goal(s) and Prove' window.
• Isabelle is started with ProofGeneral in a separate Emacs. The Isabelle file starts with the theory (declared symbols and axioms), followed by a list of theorems. Initially, all the theorems have trivial proofs, using the `oops` command. You now can replace the 'oops' commands with real Isabelle proofs, and use the Proof General button with the triagnle pointing to teh right to step through the proofs. For exmple, try (assuming that your file contains axioms Ax1, Ax2, Ax3, Ax4 and Ax5):

  using Ax1 Ax2 Ax3 Ax4 Ax5 apply(blast)

  done

Documentation of Hets.