Introduction to TabEdit

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.

Importing an assignment

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.

Entering a sentence

File/New Root Node opens a dialog box which allows you to enter an expression into a textfield. The syntax to use is

TRUE sentence. or FALSE sentence.

The sentence can contain any number of atoms and the following connectives:
~Negation
&Conjunction
|Disjunction
->Implication
<->Equivalence
The following quantifiers can be used:
ALL variable.Universal quantifier
EX variable.Existential quantifier

Example: "TRUE ALL x. (P(x) <-> Q(x))." The file format uses a very similar syntax, just that TRUE and FALSE are replaced by + and - respectively.

Constructing a proof

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:

  1. Select the element by left-clicking into the box. The color of the box turns blue.
  2. Select one of the rules from the toolbar at the bottom of the window by left-clicking onto the button.
  3. Select the target element by left-clicking into it's box.
  4. If the chosen rule was correct, new elements are generated and inserted into the tableaux. If an incorrect rule was chosen, an error message appears and no further processing can be done for a specific amount of time. This time penalty is increasing exponentially with each wrong choice!

    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.

    Example: FALSE ALL x. Q(x)
    Term for substitution: c
    Resulting sentence: FALSE Q(c)

    Example: TRUE ALL x. P(x) -> Q(s(x))
    Term for substitution: s(c)
    Resulting sentence: 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.

    Saving your work to a file

    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.

    Submitting your solution

    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.