Baumkalküle, von bzw. nach ihrem Erfinder auch Tableaukalküle bzw. Beth-Kalküle genannt, sind stark semantisch motivierte Widerlegungskalküle der Logik. Widerlegungskalküle sind solche logischen Kalküle, die nicht die Gültigkeit eines Arguments beweisen, sondern die dessen Ungültigkeit widerlegen; ein anderer, sehr bekannter Widerlegungskalkül ist der Resolutionskalkül. Der Name „Baumkalkül“ rührt daher, dass beim Ableiten in einem Beth-Kalkül eine Baumstruktur erzeugt wird. Diese Aussage ist eine Beschreibung, keine Definition, weil nicht jeder Kalkül, der Baumstrukturen erzeugt, auch Baumkalkül genannt wird. Die entstandenen Baumstrukturen werden auch Beth-Tableaux oder Beth-Tableaus (französischer bzw. eingedeutschter Plural von Beth-Tableau) genannt. In diesem Artikel soll ein Baumkalkül für die klassische Aussagenlogik vorgestellt werden: Ein Kalkül für die klassische Logik deshalb, weil die historisch ersten Baumkalküle klassisch waren; ein Kalkül für die Aussagenlogik deshalb, weil dieser der einfachste ist und die Grundlage vieler anderer Baumkalküle bildet, zunächst für den Baumkalkül der wichtigen klassischen Prädikatenlogik. Tableaukalküle gibt es auch für viele nichtklassische logische Systeme.

[Last contributor : WOBE3333 , Content under LGPL licence]