Other programs - Feedback - Deutsche Fassung
This is a beta version. The tableau algorithms always terminate, but (a) there is a bug hidden in them, and (b) there are valid arguments they are not able to derive. The algorithm from Benson Mates' book "Elementary Logic" is complete, but it leads to longish proofs, is rather slow and does not generally terminate on invalid arguments. There are a number of examples showing the syntax. Please note that the lower-case letter "v" denoting disjunction must be preceeded and followed by at least one blank character. Please note also that the upper-case letter "E" may be used as an abbreviation for the existantial quantifier. For this reason, "E" must not be used as a predicate letter.