Tableau (system dowodzenia twierdzeń)

Szablon:Dopracować 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 $\mathrm{\neg }\mathrm{\neg }x,$ możemy dodać $x,$
• jeżeli w „gałęzi” znajduje się $x\wedge y,$ możemy umieścić $x,$ a pod nim $y,$
• gdy w pewnej części „gałęzi” jest $x\vee y,$ możemy wstawić rozgałęzienie: $x$ z jednej strony, $y$ z drugiej,
• ...,
• itd., w zależności od logiki.

Jeśli w dowolnej „gałęzi”, dla dowolnego $x,$ jest jednocześnie $x$ i $\mathrm{\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.