Tableau (l. mn. tableaux) – system automatycznego dowodzenia twierdzeń polegający na konstruowaniu „drzewa” – w jego korzeniu umieszczamy formułę, której sprzeczność chcemy wykazać, mianowicie zaprzeczenie formuły, której tautologiczność chcemy wykazać.

Następnie na końcu dowolnej „gałęzi”:

• jeśli w jakimkolwiek miejscu „gałęzi” mamy ${\displaystyle \neg \neg x,}$ możemy dodać ${\displaystyle x,}$
• jeżeli w „gałęzi” znajduje się ${\displaystyle x\land y,}$ możemy umieścić ${\displaystyle x,}$ a pod nim ${\displaystyle y,}$
• gdy w pewnej części „gałęzi” jest ${\displaystyle x\lor y,}$ możemy wstawić rozgałęzienie: ${\displaystyle x}$ z jednej strony, ${\displaystyle y}$ z drugiej,
• ...,
• itd., w zależności od logiki.

Jeśli w dowolnej „gałęzi”, dla dowolnego ${\displaystyle x,}$ jest jednocześnie ${\displaystyle x}$ i ${\displaystyle \neg x,}$ oznacza to, iż otrzymaliśmy sprzeczność i gałąź ta jest zamknięta, a więc możemy pominąć tę gałąź w dalszych rozważaniach. Jeśli zamknęliśmy wszystkie gałęzie, oznacza to, że dana formuła jest sprzeczna.