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 ${\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.