TABLEAUX

This page contains an applet for constructing tableaus for predicate logic. Start the program by clicking the Start-button here on top. At first an input window pops up which contains two text fields Left and Right, as is illustrated here below:

The text fields are used to fill in the sequent that you want to start the tableau with. If you want to check the validity of an inference then you put the premises in the Left-textfield, separated by commas, and the conclusion in the Right-field. If you want to check whether a set of formulas is satisfiable (consistent) or not you have to fill in all the formulas in the Left-field.

Writing formulas

The formulas have to be filled in using your keyboard. Since there are no logical symbols on an ordinary keyboard you need the following alternative symbols:
A = universal quantifier (for all)
E = existential quantifier (some)
& = conjunction (and)
v = disjunction (or)
> = implication (if .. then)
~ = equivalence (if and only if)
- = negation (not)
For predicate letters you may use P,Q, R, S and T, and for variables x, y, z, u and w. Constants and equality (=) may not be used. Predicate letters without arguments are considered to be proposition letters as in propositional logic (this makes it possible to start with tableaus for propositional logic first).

Constructing the tableau

After you filled in the formulas correctly (the program warns you if you have made syntax errors), you start the tableau by clicking the Hopsa-button which you find under the text fields in the Input-window.

A large green colored window pops up with the starting sequent on top.

The *-symbol separates the left and the right part of the sequent.

Click on the sequent and a new window of Active Formulas pops up:

The first list represents the formulas on the left (true formulas) of the sequent and the second list the formulas on the right (false formulas). This information is very relevant since the program makes use of the short notation where only formulas that are produced in the last step appear in the tableau.

Click one of the active formulas (which contains logical symbols) and then this window disappears and the resulting step is made in the Tableau window. For making a next step click the sequent in the tableau that you want to reduce one step further, and the Active formulas-window reappears. Click in this window the formula you want to reduce this time and the step is made in the Tableau-window.

Resizing and replacing

Resize the Tableau-window if the tableau gets too large. You can do this in the way you are used to resize windows on your computer's desktop. You can also replace the tableau within the window by clicking on one of the four borders (darker green) of the Tableau window. The tableau moves towards the side where you clicked.

Closed and open branches

Detection of closed and open branches are left to the user. You can easily do so by clicking the given sequent and then look at the Active Formulas-lists. If there is a formula which appears in both lists then the sequent is obviously closed. If you have a sequent which is not closed and there are no logical symbols left in both lists then this sequent is open and represents a (counter)-model for the sequent you have started with.

Starting a new tableau

To start a new tableau just close the Tableau-window and a new Input-window appears. Fill in the text fields and proceed as before.