Tableau (system dowodzenia twierdzeń)

Ten artykuł od 2011-07 wymaga zweryfikowania podanych informacji.

Należy podać wiarygodne źródła w formie przypisów bibliograficznych.
Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte.
Sprawdź w źródłach: Encyklopedia PWN • Google Books • Google Scholar • Federacja Bibliotek Cyfrowych • BazHum • BazTech • RCIN • Internet Archive (texts / inlibrary)
Dokładniejsze informacje o tym, co należy poprawić, być może znajdują się w dyskusji tego artykułu.
Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

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 $\neg \neg x,$ możemy dodać $x,$
jeżeli w „gałęzi” znajduje się $x\land y,$ możemy umieścić $x,$ a pod nim $y,$
gdy w pewnej części „gałęzi” jest $x\lor 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 $\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.