After starting TabEdit, you will see a plain white area that will later contain the tableaux. At the bottom of the window there is a row of buttons with images of each available tableaux rule. Pressing one of the buttons will apply the rule to the currently selected element. Below the buttons the status bar contains a line of text which may be helpful if you don't know what to do.
You should save the assignment file from your personal homepage to a file in your home directory and then import the file into TabEdit by choosing File/Open from the pulldown menu. A dialog box appears and prompts you to choose the file to import. Double-clicking on the filename or selecting the file with the left mouse-button and clicking on the OK button closes the dialog box and opens the selected file in TabEdit. The sentence appears in the main area of TabEdit.
File/New Root Node opens a dialog box which allows you to enter an expression into a
textfield. The syntax to use is
TRUE ALL x. (P(x) <-> Q(x))."The file format uses a very similar syntax, just that
FALSEare replaced by
The elements of the tableaux appear as colored boxes including the sentence. There are four different colors:
To apply a rule to an element, the following steps are necessary:
When processing a quantifier a dialog is displayed, prompting for a term for substitution. Depending
on the type of quantifier you have to enter a constant or a ground term which will then be substituted
for the variable bound by the quantifier.
FALSE ALL x. Q(x)
Term for substitution:
TRUE ALL x. P(x) -> Q(s(x))
Term for substitution:
TRUE P(s(c)) -> Q(s(s(c)))
The selection of the target element can be omitted by deactivating the option Node/Always select target branch.
For large proofs you may want to select Node/Show level numbering. For each element that has been generated by applying a rule to another element, this will display the level number of it's parent.
To finish the proof, every path should be marked either finished or contradictory. To mark a path as finished, select an element by left-clicking and select Node/Mark Finished from the pulldown menu. You can also right-click on the element and select the command from the popup menu. All paths that the selected element is on will be marked finished. A path can be marked contradictory in the same way. To mark a path unfinished or non-contradictory, select the element and choose Node/Remove Mark. You can also cycle between the marks for a path by selecting Node/Cycle Mark.
To export the tableaux to a file select File/Save. In the appearing dialog box enter the name of the file and press the OK button. This file can later be imported using File/Open.
To submit the currently opened tableaux, select File/Submit. Enter your user ID,
your password and the number of the assignment into the dialog box and press the "Submit" button.
The tableaux will be submitted and you should be able to see your solution on your homepage at
http://puzzle.ics.hut.fi/T-79.3001/students/<userid>. Don't forget to reload the page in
case the file doesn't appear at once. If the file still does not appear, you may
have entered a wrong password and should try to resubmit. If that doesn't help you should look at
the error log, accessible through your homepage.