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.