The theorem prover - how it works

Part of the server side of the Gateway to Logic is a prover for classical propositional logic. If you have tried it out, you probably noticed the unusual style and the length of the resulting proofs. The reason is as simple as the prover itself:

The program uses the Beth method of deciding whether the supplied proposition is a theorem. More precisely, it constructs a Beth tableau (Beth tree) for its negation, thereby looking for a counter-example. If there is none, i.e. if the tree is closed, it prints the tableau in an at least somehow readable way: as a Gentzen/Jaskowsky style derivation.

In turn, some of the derivation rules used look a bit unfamiliar - and they use German names. Here is a list of (hopeully) all rules the program makes use of:

A

The rule of assertion is a standard rule in Gentzen-style calculi.

&B

This is the plain rule of & elimination ("B" denoting the German word for elimination - "Beseitigung")

&E

This is the plain rule of & introduction (!) ("E" denoting the German word for introduction, "Einführung"&hell;).

RAA

reductio ad absurdum (RAA) is a fairly common rule in Gentzen-style calculi. It allows to negate an assertion from which a contradiction has been derived.

DN

rule of double negation, allowing to drop a double negation.

→R

The "arrow rule" is quite typical for Beth style calculi. It allows to derive e.g. the proposition P∧¬Q from the negated conditional ¬(P→Q). Note that it is very easy to derive these argument forms using more common Gentzen-style rules. Using a dedicated "arrow rule" simply provides for shorter derivations.

De Morgan

A rule for applying the laws of De Morgan. This, too, is a dependent rule that could easily be derived from other rules.

If you want to learn more about Beth tableaux, you could consider to have a look at Wilfrid Hodges's introductory book Logic (Penguin paperback, London 1991). It is a great informal introduction to formal logic (no, that's not a contradiction in terms).