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 możemy dodać jeżeli w „gałęzi” znajduje się możemy umieścić a pod nim gdy w pewnej części „gałęzi” jest możemy wstawić rozgałęzienie: z jednej strony, z drugiej, ..., itd., w zależności od logiki.
Jeśli w dowolnej „gałęzi”, dla dowolnego jest jednocześnie i 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.
Kategoria:Automatyczne dowodzenie twierdzeń