Tableau (system dowodzenia twierdzeń)
Z Wikipedii
Tableau (l. mn. tableaux) to system automatycznego dowodzenia twierdzeń polegający na konstruowaniu drzew – 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ć x,
- jeżeli w gałęzi znajduje się , możemy umieścić x, a pod nim y,
- gdy w pewnej części gałęzi jest , 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 , 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.