Andere Funktionen - Kontakt - English version
Es handelt sich hierbei um eine Testversion. Die beiden Tableauverfahren terminieren stets, enthalten aber (a) noch einen Fehler und können (b) nicht jedes gültige Argument herleiten. Das Verfahren nach Benson Mates, "Elementare Logik", arbeitet fehlerlos und kann jedes gültige Argument herleiten, liefert jedoch meist längere Beweise, ist sehr viel rechenaufwändiger und hält bei ungültigen Argumenten nicht an.
Beispiele, anhand derer Sie sich mit der Syntax vertraut machen und mit denen Sie den Beweiser ausprobieren können, finden Sie hier. Bitte beachten Sie, dass dem Kleinbuchstaben "v" je mindestens ein Leerschritt vorangehen und folgen muss, wenn der Buchstabe die Disjunktion bezeichnen soll. Bitte beachten Sie auch, dass der Großbuchstabe "E" die Abkürzung für den Existenzquantor ist und deshalb nicht als Prädikatbuchstabe verwendet werden kann.