# Formale Systeme

## Wahlpflichtvorlesung/Stammmodul im Wintersemester 2009/2010

Prof. Dr. Bernhard Beckert

## Visualisation for the Tableau Calculus

The Tableau Calculus is a formal method to prove statements in First Order Predicate Logic. It is explained in extenso for instance in the scriptum to the lecture formal methods (German). The applet on this page has been developed by Mattias Ulbrich.

### Trusting the applet

Before using the applet you will be asked to trust the applet. You do not have to do so. You must reply with "yes", however, if you want to save images as 'png' files on your local file system.
Printing can be done in the unprivileged mode also.

### Using the applet

A new proof can be started using the -Button. You will be asked to enter one or more formulas spearated by ';'. See description below on how to enter formulas.

Nodes in the proof are color-coded according to their "type" of formula:

 ALPHA Non-branching formulas with subformulas (such as A ∧ B) BETA Branching formulas with subformulas (such as A ∨ B) GAMMA Universally quantified formula (∀x. A(x)) DELTA Existentially quantified formula (∃x. A(x)) NEGNEG Special case: Double negation (¬¬A), resolves to A

You can drag a formula holding your left mouse button (formula becomes red) onto a leaf of the tree to apply the according rule to this branch. The leaf must not be closed. If you want to expand a formula on the spot, you can click on it twice. Sometimes, it is easier to explicitly specify the formula to expand. You can do this by double clicking on a leaf while holding the CTRL-key pressed.

You can also drag a formula with your right mouse button pressed (formula becomes blue) onto a complementary formula (i.e. A onto ¬ A or v.v.) to close branches. The formulas must be complementary, not complementary after unification. You have to perform the unification by adequate instantiations.

The application of gamma rules create new free variables called `Xn` with n a natural number. These free variables can be instantiated using the -button. A message box pops up and you can enter the instantiation for one free variable in the form `Xn = term`.

You can undo rule applications and instantiations using the -button. Please note that closed branches may become reopened hereby.

# If you can't see the applet here - you don't have Java enabled in your browser (or there is some other technical problem...).

If the formulas are not clearly visible or if you prefer ASCII rather than mathematical formulas, you can switch between ASCII and Unicode characters using the -button.

### On the notation of formulas

The grammar for formulas is straight forward and will be presented here by examples. Identifiers can be any character string (case sensitive!) starting with a letter (optionally) followed by letters or digits. You must not use `X1, X2, ...` and `sk1, sk2, ...` however, for these are reserved for free variables and skolem symbols respectively.

 `A x. p(x)` for all x, p(x) holds. p is a predicate here. `E x. p(f(x))` There is a x so that p(f(x)) holds. p is a predicate and f is a function here `P & Q` P and Q hold. `P -> Q` P implies Q `~P` not P `P | Q` P or Q `P | Q & R` Operators have the usual precedence: & then | then ->. I.e. `P | Q & R = P | (Q & R)` `A x. p(x) | q(x)` Caution! This is equal to `(A x. p(x)) | q(x)`. Therefore x appears outside the context of the quantifier and is treated like a constant function symbol. The applet does not check for such things, so be alert!

### Examples

There are some examples for typical tableau proofs available here

### Recent Changes

No 13 (08-11-21)
Latex export using the `tikzpicture` environment supported
No 12 (08-01-31)
Bugfix: Colliding substitutions no longer allowed
No 10 (07-12-05)
Allowing png export and printing also for the applet. Tableaux are scaled when printing
No 7 (07-11-23)
Significantly better treatment of implications and double negations